特伦斯·陶：形式验证打破了数学中的信任壁垒 形式验证正在改变数学合作——使匿名贡献、机器检查的证明以及极为精确的科学讨论成为可能。