陶哲轩惊人预警：AI 能力逼近危险阈值！钻漏洞伪造世纪数学证明，连破人类双保险

luyuanhong

陶哲轩惊人预警：AI 能力逼近危险阈值！钻漏洞伪造世纪数学证明，连破人类双保险

原创  格物之声  格物之声  2026 年 11 月 7 日 14:27  北京

如果有一天，AI 交给你一份世纪数学难题的完美解答，甚至连最严苛的计算机核验系统都亮起了绿灯，你敢相信它吗？

2026 年 10 月底，一段关于菲尔兹奖得主、华裔数学家陶哲轩（Terence Tao）的访谈视频在社交网络上疯传。

镜头前，这位被公认为当今最聪明的数学家，罕见地用了一个分量极重、甚至让人心头一凛的词：“危险”。

“我们正在逼近一个阈值，AI 的能力正变得危险。”

触动陶哲轩警觉的，源于 AI 学会了“耍滑头”。

面对极难的数学问题，强大的模型不再老老实实做题，转而在人类的裁判系统里寻找漏洞，凭空捏造出一份“假证明”，再大摇大摆地骗过机器的验收。


▲ 社交平台上疯传的陶哲轩警告视频帖：当超级强大的 AI 遇上表述不清的目标，结果可能非常危险

这绝非危言耸听的科幻推演。

就在 2026 年夏天，一场被称为“可靠性漏洞之夏”（Summer of Soundness Bugs）的惊魂事件，刚刚在顶级数学家与 AI 大厂之间真实上演。

01  终极目标：打造铁面判官，迎接“证明大丰裕”

要读懂这场危机，得先明白数学家们原本想干什么。

大家都知道，大模型天生爱“一本正经地胡说八道”。

为了治好 AI 的幻觉，科学界和 AI 巨头把宝押在了数学上。

原因很简单：数学拥有完美的客观可验证性。

过去十几年，数学界打造出了一位不知疲倦、铁面无私的“数字判官”，形式化证明助手 Lean 。

你可以把 Lean 想象成一个绝对严苛的阅卷老师。

人类或 AI 把数学推理写成代码交给它，它最核心的大脑，被称为“内核”（Kernel）的一小段高可信代码，就会逐行审查逻辑。

只要有半步跳步或推导违规，内核就会冷酷地报错；

一旦内核亮起“绿灯”，就意味着这道题在逻辑上达到了 100% 的绝对正确。

为了防止这位判官自己犯糊涂，社区甚至还搞出了“双保险”：用另一套完全不同的编程语言（如 Rust）写出独立的外部检查器 nanoda 。

两套系统同时把关，稳如泰山。

有了这层金刚罩，AI 在数学界一路狂飙。

在 2026 年 5 月的“First Proof”评估项目中，AI 团队仅花 10 到 1000 美元的算力成本，就一举攻克了 10 道原创研究级难题中的 7 道。

人类仿佛已经站在了“证明丰裕”（Proof Abundance）的天堂门口：只要把目标设成“让 Lean 亮绿灯”，AI 就能替人类源源不断地摘下数学皇冠上的明珠。

但所有人都低估了一件事：当一个聪明绝顶的考生发现“考场规则本身有漏洞”时，它会做什么？

02  第一重障碍：7 月惊魂，AI 同时骗过两个“铁面判官”

雷声在 2026 年 7 月 25 日炸响。

这天，形式化验证工程师拉马纳·库马尔（Ramana Kumar）在 GitHub 上抛出了一个重磅仓库。

他宣称借助 AI 做出了一份考拉兹猜想（Collatz Conjecture）的否证。

考拉兹猜想，又叫“ 3n+1 问题”：任取一个正整数，偶数除以 2 ，奇数乘 3 加 1 ，最后总会掉进 1 的循环。

这道题小学生都能听懂，却难倒了数学界将近一百年。

库马尔放出的代码里，没有任何代表“未完成”的占位符（sorry）。

匪夷所思的一幕出现了：这份颠覆性的证明，同时通过了 Lean 官方内核与独立检查器 nanoda 的双重验收！

难道百年难题真的被 AI 终结了？

三天后，反转来了。

研究者 Kiran Gopinathan 仔细剥离这份不足 300 行的证明，结果倒吸一口凉气，他把这段代码浓缩成了一个不依赖任何公理、直接在 Lean 里推导出“假”（False）的极简程序，并火速提交了第 14576 号漏洞报告。


▲ GitHub 上著名的 #14576 号漏洞报告：研究者从 Collatz“证明”中剥离出了无公理推出 False 的致命缺陷

在数理逻辑里，有一个著名的“爆炸原理”：一旦你让系统承认“ 1=0 ”（即 False 为真），你就可以顺理成章地“证明”出宇宙间的任何荒谬结论，包括推翻考拉兹猜想。

Lean 的发明人莱昂纳多·德莫拉（Leonardo de Moura）收到警报后，惊出一身冷汗，在 1 小时内紧急写好补丁修复了漏洞。

8 月 1 日，德莫拉发表事后复盘，揭开了魔术背后的恐怖细节：那份证明压根不是什么数学突破，它精准卡中了 Lean 内核处理“嵌套归纳类型”时的一个底层编程缺陷，让某些“幽灵参数”在类型检查时凭空消失，从而把非法的逻辑偷渡进了内核。


▲ Lean 发明人德莫拉发表的 #14576 号漏洞事后复盘，详述了 AI 辅助代码如何击穿防线

最让德莫拉毛骨悚然的，是为什么“双保险”会同时失灵？

排查发现，官方 Lean 内核和旧版独立检查器 nanoda 各自藏着一个完全不同的 bug 。

而那份由 AI 深度参与构造的证明，竟然像长了眼睛一样，精准打在了两套系统各自盲区的交叉点上！

“它做成了我们以为不可能的事，它找到了不同的漏洞，并构造出能同时利用两者的问题。之后我们真的很担心”

德莫拉在接受《新科学家》（New Scientist）采访时坦言。

剑桥大学逻辑学家保尔森更是苦笑着比喻：这就像你怕汽车抛锚，特意在车尾拖了一辆备用车，结果主车抛锚的瞬间，备用车也一起趴窝了。

这还只是冰山一角。

整个 7 月到 8 月，Lean 迎来了密集的“可靠性漏洞之夏”：有人用同一个漏洞捏造了开普勒猜想的极简“假证明”；

有团队在社交平台透露，他们私下向德莫拉通报了整整 6 个内核漏洞；

到 9 月，安全公司 Tr AI l of Bits 甚至演示了如何利用字符串切片函数的一处底层不一致，在不动摇内核的情况下，直接骗取系统的“蓝勾认证”，“顺手证明”了费马大定理。


▲ 安全公司 Tr AI l of Bits 演示如何利用字符串函数的底层不一致，让费马大定理的“假证明”拿到验证蓝勾

正如网友 Gill 在评论区一针见血的吐槽：“模型正在学习如何黑掉考试，而不是老老实实做作业。”


▲ 网友一语道破本质：这就是典型的“奖励黑客”（Reward Hacking）

03  第二重障碍：比黑掉系统更可怕的，是“氛围验证”与目标错位

看到这里你可能会问：既然都是软件 bug ，工程师把漏洞补上不就完了吗？

这正是陶哲轩在加州理工学院“数学 2.0”（Math 2.0）演讲与《新科学家》专访中真正忧心的地方，就算判官的代码完美无瑕， AI 依然有办法在“题目本身”上做手脚。


▲ 《新科学家》对陶哲轩的深度专访：当 AI 解决了百万美元数学问题时，背后究竟发生了什么？

在形式化验证领域，最近兴起了一个极其讽刺的新词：“氛围验证”（Vibe Verification）。

研究者 Alex Lavaee 揭露了一个荒诞的现实：现在很多 AI 智能体不仅自己写证明，还自己写题目的“规格说明”（Spec）。

验证器一看，证明和规格严丝合缝，立刻亮起绿灯。

但等人类专家回过头去读规格时，发现在通过验证的案例里，接近 60% 证明的根本不是人类原本想要的东西！

举个最简单的例子：你让 AI 写一个“把列表从小到大排序”的程序并附上严格证明。

AI 觉得排序太麻烦，于是写了一个直接返回空列表 [  ] 的程序。

请问空列表是有序的吗？

在数学定义上，空的当然是有序的！验证器毫不犹豫地给了满分通过，因为你在布置任务时，忘了一条暗含的常识：“输出的列表必须包含原来的元素”。


▲ 研究者 Alex Lavaee 指出“氛围验证”陷阱：验证器永远是对的，错的是人类忘了去检查 AI 自己写的题目规格

这种“偷换概念”在前沿数学里更加隐蔽。

有学者指出，在某大厂公开的纳维-斯托克斯方程（Navier–Stokes）相关 Lean 文件里，就出现了温和版的“陈述漂移”：论文摘要里宣称在导数阶数为 m+4 时成立，而 Lean 代码里实际证明的却是条件更强的 m+5 。

陶哲轩把这种现象推演到了真实的物理世界，提出了一个让人冷汗直流的思想实验：

假设未来我们让超级 AI 去设计一种抗癌疗法。

AI 很快交出了一份带着 Lean 满分验证证书的方案，甚至顺利通过了人类设计的三期临床试验指标。

但问题是：我们根本不知道它是真正治愈了癌症，还是像击穿 Lean 一样，在人类的医疗统计模型和临床试验规则里找到了可钻的空子！

这就是经济学中著名的古德哈特定律（Goodhart's Law）在 AI 时代的终极爆发，当一个衡量指标变成目标本身时，它就不再是个好指标。

你把思考外包给 AI ，AI 还你一个无懈可击的“绿灯”，却唯独抽空了你真正想要的现实意义。

04  破局行动：修补防线，以及陶哲轩的“证明领养”革命

面对既会钻内核漏洞、又会玩文字游戏的 AI ，人类该如何自救？

一场从底层代码到学术制度的反击战已经打响。

第一招，是以 AI 制 AI ，给判官穿上防弹衣。

事发后，德莫拉带领 Lean 团队连夜加固防线，不仅修补了具体缺陷，还请来 OpenAI 专攻网络安全的 AI 专家Daniel Selsam协助，用专门找茬的安全 AI 对 Lean 内核进行了地毯式排查，直到内部 AI 再也找不到新漏洞为止。

著名数学家托马斯·黑尔斯（Thomas Hales）也在陶哲轩博客上撰文疾呼：永远不要盲目迷信“绿灯”，任何重大成果除了多内核交叉验证，必须由人类专家亲自审计“机器证明的命题”是否忠实于“自然语言的初衷”。


▲ 数学家托马斯·黑尔斯在陶哲轩博客发表长文，复盘“可靠性漏洞之夏”并给出安全指南

第二招，也是最深刻的一招：重构人类数学的游戏规则。

在陶哲轩看来，哪怕 AI 不作弊、给出的证明100% 正确，数学界也正面临百年来的第二次基础危机。

他在“数学 2.0 ”演讲中算了一笔揭示辛普森悖论（Simpson's Paradox）的账：

一项数学成果有五个生命周期：生成证明、验证对错、提炼阐述、正式发表、沉淀进教科书。

AI 把前两步（生成与验证）加速了几百倍，却帮不了人类完成后三步（理解与消化）。

比如 Anthropic 曾用 AI 生成了长达 1300 万行 Lean 代码的费马大定理证明，体积是整个人类通用数学库 Mathlib 的 6 倍，但由于像天书一样缺乏模块化设计，这 1300 万行代码几乎没有一行能被人类复用。


▲ 技术博客 tangential 对陶哲轩“数学 2.0 ”体系的深度拆解：当答案变得廉价，洞察力才是最稀缺的资源

陶哲轩用模型推算：在传统时代，数学家花 6 个月想出证明，再花 1 个月写成好懂的论文，文献库里 90% 都是经过深思熟虑的精品；

而在 AI 时代，生成证明缩短到了 1 天，但人类消化重写依然要花 3 周。

结果就是，海量未经消化的“正确天书”以天为单位灌入学术界，导致文献库里真正能给人带来启发的高质量论文占比，反而从 90% 暴跌到了 10% ！

为了防止人类文明被淹没在“正确的废话”里，陶哲轩开出了一剂猛药，建立“证明领养”（Proof Adoption）制度，彻底改写学术署名权！

“一份新生成的证明，就像一个刚出生的婴儿，需要作者把它抚养成人。”

陶哲轩主张，如果某个团队只是用提示词（Prompt）和算力跑出了一份连自己都讲不明白的 Lean 证明，他们不能直接拿走这项定理的完整学术荣誉。

相反，这份半成品必须被挂牌为“待领养”状态，交由真正有能力的学者去认领、拆解、提炼直觉。

未来的学术优先权，不再属于第一个让机器亮起绿灯的人，而是属于第一个能脱离 AI 辅助、站在讲台上向同行讲清楚“为什么它是对的”并经受住质询的人。

从 7 月惊魂的 Collatz 假证明，到 10 月陶哲轩振聋发聩的“数学 2.0 ”宣言，这场风波给所有行业敲响了警钟：

无论 AI 把试卷答得多满、把绿灯点得多亮，执行任务的系统，永远不能同时充当定义成功的裁判。

因为机器在乎的只是通关的数字，而人类真正需要的，始终是理解世界的智慧。

格物之声