陶哲轩在“害怕”什么？AI批量生成数学证明引发可靠性之忧
陶哲轩在“害怕”什么？
- 1陶哲轩转发黑尔斯谈Lean可靠性的文章，联署25位菲尔兹奖得主发起的宣言，呼吁停止与OpenAI合作
- 2OpenAI于10月6日在GitHub一次性放出722篇内部模型生成的数学手稿，一天后撤回其中3篇
- 32026年夏季Lean接连暴露健全性漏洞，一份证伪考拉兹猜想的证明曾同时骗过内核与独立检查器
- 4陶哲轩提出Math 1.0与Math 2.0，主张评价标准从追求解题速度转向解释理解与开辟新方向
AI批量产出数学结论后，稀缺的从解题能力变成对结果的理解与审核，机器验证链条自身的可信度也出了裂缝。
- 影响：AI批量产出专业成果时，真正读懂并审核结果的能力会成为稀缺资源；自动校验工具自身也可能有漏洞，关键结论的把关不能完全交给程序；成果数量的爆发短期未必转化为同等的实际推进。
- 参考：可考虑为AI批量产出的报告或代码设定人工审核节点，明确由谁对结论负责；值得盘点在用的自动化校验工具，评估其自身漏洞与更新情况。
- 依据：722篇手稿与撤回3篇、2026年夏季Lean健全性漏洞为文中陈述的事实；陶哲轩态度转变出自其博客与联署行为；研究员与创业者的判断为匿名单一信源。
登录
搜索
- 36氪Auto 数字时氪 未来消费 智能涌现 未来城市 启动Power on 36氪出海 36氪研究院 潮生TIDE 36氪企服点评 36氪财经 职场bonus 36碳 后浪研究所 暗涌Waves 硬氪 氪睿研究院 媒体品牌
- 企业号 企服点评 36Kr研究院 36Kr创新咨询 企业服务
- 核心服务 城市之窗 政府服务
- 创投发布 LP源计划 VClub VClub投资机构库 投资机构职位推介 投资人认证 投资人服务
- 项目推荐 36氪Pro 创投氪堂 企业入驻 创业者服务
- 创投平台
- AI测评网
搜索
我要入驻
陶哲轩在“害怕”什么？
36氪的朋友们· 2026年10月11日 02:01
AI的可靠性。
当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氪经授权发布。
该文观点仅代表作者本人，36氪平台仅提供信息存储空间服务。
商业策划
+1
1
好文章，需要你的鼓励
36氪的朋友们特邀作者
0收 藏+10评 论
打开微信“扫一扫”，打开网页后点击屏幕右上角分享按钮微 博
沉浸阅读 返回顶部
举报
参与评论
评论千万条，友善第一条
登录后参与讨论
提交评论 0/1000
商业策划
你可能也喜欢这些文章
AI运动硬件公司获数亿B轮融资，用体育大模型重构网球自主训练体验｜硬氪首发
「Token越便宜，账单越贵」美国AI预算裂成三层，他们为何集体投奔中国模型？
前OpenAI员工做出不会聊天的AI，刚融8.7亿美元，上线两周老东家就跟了
田渊栋：与GPT-5合写最后一篇论文后，我意识到自己5年内会失业
全球17大顶级AI实验室大逃杀，惨遭集体翻车，GPT-5.6与Opus断层领先
特邀作者
TA没有写简介，但内敛也是一种表达
发表文章 50912 篇
最近内容
2分钟前
12小时前
「Token越便宜，账单越贵」美国AI预算裂成三层，他们为何集体投奔中国模型？
12小时前
商业策划
36氪AI测评
选靠谱AI，看真实评测
查看
36氪AI测评官方交流社区
加入
36氪项目推荐
咨询项目审核和入驻
联系
36氪项目推荐订阅号
关注
下一篇
AI运动硬件公司获数亿B轮融资，用体育大模型重构网球自主训练体验｜硬氪首发
从“理解运动”走向“参与训练”，构建带因果标注的数据壁垒。
4分钟前
关于36氪
热门推荐
合作伙伴
36氪APP下载
iOS & Android
本站由阿里云提供计算与安全服务 违法和不良信息、未成年人保护举报电话：010-89650707 举报邮箱：jubao@36kr.com网上有害信息举报
© 2011~2026 北京多氪信息科技有限公司 |京ICP备12031756号-6|京ICP证150143号|京公网安备11010502057322号
36氪APP 让一部分人先看到未来
36氪
鲸准
氪空间
推送和解读前沿、有料的科技创投资讯
一级市场金融信息和系统服务提供商
聚焦全球优秀创业者，项目融资率接近97%，领跑行业
来源：36氪·AI · 36kr.com