AI 生成数学结论的验证问题与数学发展的新危机

2026 年 10 月 6 日，OpenAI 发布了 722 份数学手稿，分为 372 组相关结果。这是手稿数量和结果分组，并不等于 722 个已经得到学术确认的新定理。OpenAI 明确说明，这些结果处于不同的核验阶段，并非全部附有 Lean 形式化证明。10 月 7 日，人类数学协会在陶哲轩博客上发表声明，批评这种集中发布方式，强调数学研究应当以人的理解为中心。这份声明是协会署名的客座文章，不能直接视为陶哲轩个人对全部手稿的判断。[1、2、3]

这场讨论提出了一个具体问题。AI 可以快速生成数学结论和证明文本，但人类能否以同样的速度确认它们的正确性，并理解它们在数学中的意义？我认为，这确实可能形成数学发展的一次新危机。要判断危机发生在哪里，需要区分生成结论、验证证明和理解方法这几件事。

AI 在不同领域生成的结果，其成立标准并不相同。一幅图像、一段音乐或一篇文学作品，可以通过作品本身的效果接受评价。我们可以讨论它是否合适、是否有感染力，而不必先复原生成过程。一段程序则可以通过运行和测试检查部分功能，但测试通过并不保证所有输入下都正确。工程和实验科学还要检查结果是否符合实际条件，能否通过独立实验或观测得到支持。因此，其他领域同样存在验证问题，不能因为结果能够使用，就认为其中的事实和推理已经可靠。

数学定理提出的要求更严格。它主张，在给定的定义和假设下，结论对规定范围内的全部对象成立。大量计算结果可以支持一个猜想，却通常不能代替一般性证明。即使前一百万个例子都符合，也不能由此排除后面的反例。经验科学可以通过新的观测修正理论，数学中的普遍命题则需要交代从前提到结论的有效推导。

反例与一般性证明之间也存在不对称。对于“所有满足条件的对象都具有某种性质”的猜想，一个经过严格核验的反例就足以否定它。但寻找反例本身未必容易，反例是否满足全部条件也需要证明。因此，AI 找到反例可以构成真正的数学贡献，却不能由此推断多数 AI 数学成果都是反例，或者否定性结果都容易核验。

数学的特殊性还在于，定理之间具有明确的依赖关系。一项结果可能成为另一项证明的前提。如果未经充分核验的结果被当作已成立的定理使用，错误就可能沿着依赖关系扩散。这次发布已经出现了一个实际例子。OpenAI 的更新记录显示，10 月 7 日，一份关于代数几何的手稿因符号错误导致关键论证失效，两份依赖该构造的手稿也随之撤回，共撤回三份。这个事实不能证明其他手稿都有问题，却说明不能把发布数量直接当作已确认的数学进展。[4]

我最初说 AI 是一个黑箱，需要把这句话的范围说清楚。模型内部怎样搜索、选择和形成一个结论，与它对外提交了什么证明，是两个问题。我们通常不能从输出完整复原模型内部的发现过程，但这不等于 AI 无法提供可以检查的证明。OpenAI 此次公开了部分结果的推理摘要和许多证明的形式化材料，同时也承认核验尚未覆盖全部结果。[2]

人类数学家也可能先凭直觉、类比或偶然发现得到结论，再整理证明。别人接受这个定理，不需要复原发现者大脑中的全过程，却必须能够检查公开的论证。因此，对 AI 的合理怀疑，应当落在它是否给出了充分的成立依据。内部发现过程不透明，会增加研究和解释的困难，但不能单独作为否定结论的理由。

形式证明可以解决其中一部分困难。Lean 这类工具能够依据明确的规则检查形式化证明。在这里，AI 负责生成候选证明，专门的证明检查器负责判断它是否通过；这与让另一个聊天模型说“我也认为正确”有根本区别。数学证明的检查并不必然要求人逐行手工重算。把所有核验都限定为人工操作，会忽略形式化本身带来的能力。

但形式校验也有明确边界。它检查的是写入系统的命题及其证明。定义是否准确，假设是否完整，证明的命题是否对应论文声称解决的问题，仍需要审查。比如，原问题要求对所有对象成立，形式命题却增加了一个限制条件，那么通过检查也不能证明原问题已经解决。数学家 Thomas Hales 在陶哲轩博客发表的文章中特别强调，除了证明检查，还应由人审查形式命题与原意的对应关系；这项工作通常比手工检查整个证明容易得多。[5]

这里还必须区分正确性和理解。一个完整且可靠的形式证明，即使很长、很难读，也不会因为暂时缺乏简洁解释就失去效力。但它为什么成立，关键结构在哪里，哪些条件可以放宽，方法能否迁移到其他问题，仍可能没有被人理解。确定一个命题成立，与把证明转化为能够讲解、修改和继续发展的方法，是不同层次的工作。

传统的数学研究通常把这些工作联系在一起。数学家在寻找证明时逐步形成理解，再通过写作、交流和审稿使这种理解进入共同知识。这个过程并不总是顺畅，也不要求每个人理解所有证明，但每项重要结果需要有人能够解释其关键步骤、条件和用途。AI 的批量生成可能使这些工作分离。结论和证明文本可以先大量出现，核验、解释与研究位置的判断随后交给其他人完成。

这就是生成速度超过人工验证速度时的实际问题。对没有形式化证明的手稿，专家阅读仍可能成为瓶颈；对已经可靠形式化的结果，逐步推导的检查可以加速，但命题核对、解释和方法理解仍需要时间。陶哲轩关于 AI 的公开观点也区分了生成、验证和消化结果，并指出生成和验证的加速未必同时带来理解的加速。[6]

持续的速度差会产生几种后果。未经确认的主张积压，研究者难以判断哪些结果可以安全引用；少数领域专家的时间被大量核验工作占用，自己的研究受到挤压；已经通过形式检查的证明也可能长期缺乏解释，使定理数量增长与人的方法积累脱节。生成者如果只公布“解决了多少问题”，却不承担后续修订和解释的责任，就把相当一部分研究成本转移给了数学界。

这些后果可以构成数学研究实践中的危机，但不能直接称为数学逻辑基础已经失效。生成得快，不会使一个有效证明变得无效；尚未核验，也不等于已经证明错误。同样，一次发布数百份手稿，足以提出验证能力是否跟得上的问题，却不能单凭数量认定整个数学领域的核验速度已经全面落后。真正需要观察的是，未核验结果是否持续积压，错误是否被继续引用，以及可靠证明能否进入人的理解和后续研究。

因此，AI 数学成果的发布应当同时交代命题、假设、证明依赖和核验范围。声称某项结果通过形式检查，就应公开对应的形式命题和可复核材料。发布者还应解释关键方法、回应质疑并维护修订记录。数学界可以借助机器完成大量规则检查，把人的精力集中于命题是否准确、方法是否被理解，以及成果能否支持进一步研究。

我的判断是，不能盲目接受 AI 生成的数学结论，也不能仅凭生成者是 AI 就否定它。人类数学发展面临的新风险，是结论、证明、核验和理解之间的联系被批量生成打断。当生成速度长期超过验证与理解的能力时，数学界获得的可能首先是大量待处理的主张，而不是同等规模的可靠知识。对数学进展的评价，必须把后面的工作一起计算进去。

参考来源

[1] https://community.openai.com/t/first-look-at-mathematics-manuscripts-from-an-internal-frontier-model-at-openai/1403886
[2] https://openai.com/index/sharing-ai-progress-in-mathematics/
[3] https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-openais-october-6-release-of-mathematical-documents/
[4] https://github.com/openai/math/blob/main/history.md
[5] https://terrytao.wordpress.com/2026/10/09/what-mathematicians-should-know-about-the-lean-theorem-proverquestions-of-reliability-and-ai/
[6] https://teorth.github.io/tao-web/ai-views.html