AI形式化证明能消除数学错误吗?

看到“AI完成了机器检查的数学证明”，我最想追问的不是它写了多少代码，而是：机器说通过，究竟保证了什么？我的判断是，AI形式化证明能大幅压缩某些数学错误的藏身空间，但“从此数学不会出错”，说得太满了。

AI负责寻找，检查器负责把关

我们读数学证明时，常会遇到“显然可得”。这几个字有时省略了常规推导，有时却遮住了真正的漏洞。形式化证明的价值，就是让这些跳步不能只靠读者点头放行。

这里要分清角色：AI可以提出证明、补充中间步骤，也可能走错路；Lean这样的证明助手则按照严格规则检查提交的证明。可靠性的关键，不是AI突然变得不会犯错，而是错误的推导不能轻易通过检查。当然，这个保证以检查机制正确运行、证明完整提交为前提。

证明正确，不等于题目写对

我觉得最容易被忽略的，是自然语言与形式化表述之间的缝隙。我们原本想证明一个结论，翻译时却可能缩小了讨论范围，或加入了原题没有的前提。此时机器检查通过，也只能说明“写进去的命题成立”，不能说明“我们想问的问题已经解决”。

假设同样需要审视。形式化证明保证的是：在所采用的公理和前提下，结论能够推出。它不会替我们判断额外前提是否合理，也不会自动赋予结论现实意义。

所以，看到“机器验证通过”，我会继续看：形式化命题是否忠于原意，依赖的假设是否交代清楚，证明是否完整，是否能被独立复核。代码规模再壮观，也替代不了这些问题。

我愿意把AI形式化证明看成一道更严格的质量关，而不是数学的“免检证书”。它让推理更可核查，也让人的注意力转向另一件重要的事：我们到底证明了什么，而不只是证明有没有通过。