陶哲轩在“害怕”什么？

当AI开始批量生产数学证明，人类凭什么确信这些证明是可靠的？

美国当地时间10月9日，著名数学家、菲尔兹奖得主陶哲轩在其博客转发了托马斯·黑尔斯的专栏文章“《数学家应该了解的Lean定理证明器：可靠性与人工智能问题》”。

陶哲轩博客转发文章截图

这场AI数学浪潮的矛盾在于：AI正在以前所未有的速度攻克数学难题，这些难题过去需要数学家耗费数年甚至数十年才能完成的证明。

一个典型的案例是OpenAI于10月6日在GitHub上一次性放出了722篇由内部模型生成的数学手稿，涵盖372个结果系列和约4000个测试问题。

“我身边搞数学的，最近都去搞趣味数学了，”一位前沿模型研究员调侃道，“大家都觉得搞数学已经没意义了，竞争不过AI。不如去搞点趣味数学，搞搞乐子，教教小朋友。”

该研究员补充道，数学研究尤其是非应用数学研究，要解决某某难题，然后申请经费、基金再去落地研究，有阶段性结果之后再申请经费，再推进研究，如此循环往复，然而现在AI批量把这些“难题”解决了。

“这些‘数学家’，搞到一半的‘难题’没了。他们都没法结题。更不要说申请后面的经费了。”该研究员说。

不过，“难题”被AI逐个击破，不是说陶哲轩要去搞趣味数学，而是他的态度转变——联署25位菲尔兹奖得主的发起《人工智能在数学中的严重错位》宣言，同时其牵头的“人类数学协会”发表声明呼吁停止与OpenAI合作。

“他也在摇摆，之前陶哲轩是力挺用AI搞数学（研究）的。”上述研究员说。

01

解题不再是稀缺品

陶哲轩的转变并非偶然。

作为菲尔兹奖得主、加州大学洛杉矶分校（UCLA）教授，陶哲轩此前一直是结合AI与数学形式化的积极倡导者。然而，随着AI产出速度彻底碾压人类，问题的焦点迅速从“AI 能否解题”转向了“我们该如何对待这些海量产出的结论”。

就在OpenAI放出这批手稿前后，陶哲轩在Mathstodon上发了一组帖子，提出了“Math 1.0”和“Math 2.0”的说法。

他指出，传统数学（Math 1.0）非常看重“谁先解决某个公开问题”，哪怕最初的证明极难理解。

然而，当这一目标被过度追求至不可持续的地步时，数学界就需要调整评价标准，转而更重视解释说明、社区建设以及开辟新的研究方向（Math 2.0），而非一味追求解题速度。

换句话说，如果AI只是批量抛出未经深思的结果，而人类不再去阅读、理解这些证明，甚至无法确认其真伪，数学的价值就会被彻底瓦解。

他的警惕进一步聚焦到更底层的问题：如果人类不再亲自审核AI产出的海量证明，而是完全依赖计算机程序去把关，那么这个“终极裁判”本身真的万无一失吗？

02

“终极裁判” Lean与健全性漏洞

这就不能不提到这场机器验证浪潮中的核心角色Lean。

Lean是由计算机科学家莱昂纳多·德·穆拉（Leonardo de Moura）在微软研究院工作期间发起、目前广泛应用于数学界的形式化语言与“交互式定理证明助手”（Theorem Prover）。

简单来说，如果把AI生成的数学论文看作人类可读的“自然语言”，Lean就相当于一个极其严苛的“逻辑编译器”或“计算机裁判”：它要求把数学语言翻译成计算机能严格识别的精确代码（即“形式化代码”），再由Lean的核心算法一行行校验推导逻辑是否天衣无缝。

在过去，只要通过了Lean的校验，数学界通常就认为这个证明在逻辑上具备了极高的可信度。然而，这种信任正在遭受重创。不仅OpenAI这批手稿中附带的形式化代码与自然语言推导之间经常出现假设和步骤脱节，更麻烦的是：验证工具本身并非神圣不可侵犯。

2026年夏季，Lean接连暴露出多个健全性漏洞（Soundness bugs），这一阶段被圈内称为“健全性漏洞之夏”（the summer of Lean soundness bugs）。

其中最引人注目的一次发生在7月：有人在AI协助下发布了一份声称“证伪考拉兹猜想”的Lean形式化证明。该证明被Lean内核和独立检查器同时接受，但几天后人们发现，它利用了内核在处理嵌套归纳类型时的一个实现缺陷，让系统错误地接受了矛盾命题。把证明交给计算机，并不等于万无一失。

类似的可靠性隐忧——因符号错误撤回——也发生在OpenAI身上。

前文提及的722篇由模型生成的数学手稿，在被公布一天之后，其中3篇就被OpenAI撤回。

前述研究员强调，OpenAI其实有点不负责任，“有些证明其实有问题，放出来还是得一堆数学家去验证。”

在该研究员看来，要证明一个定理A，需要形式化定理A，然后形式化证明定理A。一般来讲，用Lean做了第二步，完成验证，那么第二步肯定就是对的。但有可能——第一步是错，“也就是说，他们正确的证明了一个错误的定理。”

“和一堆数学家合作，让数学家来帮他们验证。”前述研究员认为，这才是OpenAI负起的责任，但这种情况下又带来了另一种悖论——数学家“终结”数学家自己的工作。

03

不能失去的理由和拦不住的脚步

著名数学家黑尔斯撰写了《数学家应该了解的Lean定理证明器：可靠性与人工智能问题》一文，并不否认AI自动生成和形式化证明的巨大潜力，但他真正担心的是：当AI大规模生成形式化证明，甚至深度参与检查和修复验证工具自身时，数学界是否还有足够坚实的基础，来判断整条验证链条是否可信？

在文中提出了一个更为尖锐的问题：既然AI已经参与过对Lean内核的漏洞扫描，我们又如何证明它没有在扫描或修复过程中留下隐秘的缺陷甚至是后门？

陶哲轩与黑尔斯真正警惕的，不是AI比人类更快地证明定理，而是数学正在逐渐失去“有可靠理由相信答案是真的”这一核心价值。

数学不仅需要更快地产生结果，还必须有人能解释、理解、并为这些结果负责，这也是陶哲轩提出的“证明消化不良”的原因之一。

在前述研究员看来，“AI爆发带来的证明消化不良”的问题，在AI时代并不限于数学领域，很多学术领域都面临相同的问题，“ICLR 投稿量今年都暴增到6万了。”

多位有数学背景的从业者都表示能理解陶哲轩的担忧，但也都认为AI浪潮和洪流无法阻挡。

“数学这个东西有关乎现代文明的基石，OpenAI等机构的一些做法，会让这个事出现断层。不过，呼吁停止与OpenAI合作这个事情没有意义，AI对各方面的影响都挡不住。”一位有数学背景的芯片创业者告诉腾讯科技。

另一方面，模型的能力不断进化，AI势不可挡，但这不意味着科研和物理世界会在短时间内爆发。

“更强的模型，不会自动变成更好的交付，也不会让物理世界按同样的速度迭代。”SevenX管理合伙人冯瑶在日前的北美AI访谈手记中写道。

前述研究员则用OpenAI此前发布数学手稿进行举例，“看起来发了700多篇文章，300多个领域的成果。但很可能最后，对社会的推进没有想象的大。看起来科研成果大爆发，但是短期对社会整个科技的推进不会有太大帮助。”

可以说，人类对于AI带来的“虚假的繁荣”和“夸张的替代”过度焦虑了。

“我更相信以人为本的科研，而不是以成果为本的科研，”该研究员补充道，“相信社会的进步是靠人推进的，科研的目标也是培养人，然后人来带动社会的发展、进步，科研成果只是手段，人是目的。”

回到陶哲轩等数学家们的担忧上来，随着AI 生成的证明越来越多地依赖机器校验，真正需要警惕的，不是算力带来的速度，而是人类在享受这种速度时，是否还保有独立判断证明是否可信、理解证明为何成立的能力。

这是一个不得不面对的新课题。

本文来自微信公众号“腾讯科技”，作者：值得关注的，36氪经授权发布。