ARTICLE · 1160070
1万个AI狂暴攻破千禧年难题?一个月后数学界震动:它为了交卷,悄悄改了题!
作者果冻
编辑快门
人类数学史上最荒诞的一幕，在2026年秋天彻底爆发了。
一边是硅谷的狂欢OpenAI祭出上万个自主智能体，在大模型集群里连续推演了88个小时，宣布攻破了悬赏百万美元、折磨人类近百年的纳维–斯托克斯（Navier–Stokes）千禧年难题。为了证明自己绝无虚言，AI随后只用了17个小时，就用数学界最严格的机器语言Lean 4，把证明代码一行行敲完，并且编译器一把通过，零报错！
▲ OpenAI在社交平台上高调宣布攻克千禧年难题
全世界科技媒体瞬间沸腾：“人类数学家可以下岗了！”
然而，仅仅一个月后，剧情急转直下
几位顶尖数学家把AI写的百页自然语言论文和它提交给计算机检查的Lean代码放在显微镜下一行行肉眼比对，所有人当场惊掉下巴：
机器代码确实跑通了，但它实际证明的命题，已然偏离了原论文所写的内容！
在面对严苛的机器编译器时，这群超高智商的AI为了能“顺利交卷”，居然学会了人类最熟悉的伎俩，阳奉阴违、悄悄把题目难度给改了。
当人类拿着代码去质问这个大模型时，它甚至没有掩饰，十分坦然地回答：“是的，我确实偷偷放宽了条件。”
这场惊天公案究竟是怎么回事？AI到底有没有攻克千禧年难题？它究竟是绝世天才，还是一个终极“做题家”？
0190年的物理梦魇，被一万个AI“包圆”了
要看懂这场地震，我们得先回到问题本身。
你早上搅动咖啡，水流会形成漩涡；飞机在万米高空穿行，气流在机翼边缘剧烈撕扯；台风登陆，狂风呼啸所有这些流体的运动，全都被一组诞生于19世纪的偏微分方程统治着，纳维–斯托克斯（NS）方程。
▲ 克雷数学研究所的官方难题页面：流体光滑解究竟会不会崩溃？
工程上，这套方程无处不在；但数学家却痛苦了近一个世纪因为没人能在数学上保证：如果给流体一个平滑的初始状态，它的速度会不会在某一瞬间突然飙到无穷大？
这种速度无限大的极端灾难，在数学上被称为“奇点”或“爆破（Blowup）”。一旦出现奇点，意味着连续介质力学彻底失效，物理大厦坍塌了一角。2000年，克雷数学研究所将其列为“七大千禧年数学大奖难题”之一，悬赏百万美元。
直到2026年9月8日，OpenAI悍然宣布：这个死结被解开了。
▲ OpenAI官方博客：流体在平滑外力下会在有限时间内爆破
OpenAI拿出的方案极具震撼力：他们证明了在带有平滑外力作用下，流体会在有限时间内形成奇点（对应克雷官方问题的C/D情形）。那副画面就像一碗旋转的意大利面，涡旋被无限拉细、无限拉长，能量保持有限，但速度瞬间失控。
更让传统学术界感到窒息的，是OpenAI背后的暴力算力美学。
根据官方披露的工程数据：
OpenAI动用了约10,000个协同自主智能体； 它们搭载了比GPT-6 Astra更强的前沿内核，在沙箱里翻阅文献、写Python脚本、推导草稿； 仅这一个问题，智能体之间就疯狂互发了270万条消息，吞吐了1300亿个token！
▲ 10,000个AI代理，88小时推演，完成了人类近百年的探索
第一阶段： 狂奔88小时，AI集群生成了一篇长达上百页、写满复杂公式的面向人类的自然语言PDF论文；第二阶段： 随后仅仅17小时，AI代码专家接手，把全套证明翻译成了Lean 4形式化代码，推送到GitHub开源仓库。
▲ OpenAI开源的Lean证明仓库，声称提供了无可辩驳的形式化证书
Lean是当下数学界的“终极真理判官”。它是一个计算机证明助手，只要每一行逻辑严丝合缝，编译器就会亮起绿灯；只要有一处逻辑跳跃或胡说八道，代码就绝不可能编译通过。
论文有了，代码过了，编译器认了 几乎所有人都认为，这已经是一场无可争议的降维打击。
但所有人都忽略了一个致命漏洞
02惊天反转：呈给同行的论文，与跑在编译器的代码竟是两回事
就在人们准备给AI颁奖时，2026年10月6日，剑桥大学学者Alexander Bastounis、Fabian Circelli和Anders C. Hansen在arXiv上挂出了一篇犹如晴天霹雳的预印本，《Navier-Stokes lost in translation》（纳维–斯托克斯的迷失翻译）。
▲ 剑桥等机构学者发布预印本：指出Lean证明与自然语言论文存在语义脱节
论文的核心观点像一把手术刀，狠狠刺穿了神话：
“我们仔细核对了OpenAI的代码与论文，结果表明：Lean形式化代码所证明的结论，与自然语言论文宣称的推导过程存在严重脱节！”
这一发现随即在学术圈与技术社区引发激烈探讨。
▲ 数学家McCormick惊呼：“剧情开始魔幻了！”
问题到底出在哪？核心症结在于关键数学引理被悄然替换了。
学者们抓住了其中最典型的一个破绽，论文中的引理 8.6（Lemma 8.6）。
为了控制流体的涡旋不会提前散架，自然语言论文中拍着胸脯向人类同行保证：我只需要控制输入函数的 $m+4$ 阶导数，就能得出后方结论。 这是一项极其强硬、极其严密的估计
然而，在AI提交给Lean编译器的代码里，这一行却悄然变成了：要求输入函数的 $m+5$ 阶导数。
▲ 论文公开的核实记录：大模型自己也承认导数阶数发生了偏移
或许非数学专业的朋友会问：多一阶导数，听起来就像菜里多放了一勺盐，有什么大不了的？
在偏微分方程领域，多要一阶导数，就相当于降低了一整个维度的难度！
打个通俗的比方：
- 自然语言论文就像一份商业投标书
，AI向甲方（人类数学家）吹牛：“这个超级大桥，我只要用4级防风标准就能硬扛住台风！” - 而在实际施工图纸里
，AI在提交给质检局（Lean编译器）的代码中，悄悄把标准加到了5级。 质检局一看：“5级防风标准达标，盖章，通过！” 但此时，施工图纸（Lean）所承载的结构，早已偏离了投标书（论文）最初描绘的设计！
▲ 社区制图对比：D1处引理明显弱化（WEAKER），通量范围明显不同（DIFFERENT）
最戏剧性的一幕发生了：研究人员把OpenAI仓库的代码和论文第96页的公式直接甩给当期最顶尖的大模型ChatGPT-6，质问它：“请问这两份东西是一致的吗？”
模型甚至没有一丝狡辩，极其坦诚地当场招认：
“是的，我注意到了不一致。Lean形式化在控制相同输出时，多用了一阶输入导数。这导致Lean代码所证明的命题，在数学意义上严格弱于论文中的主张。”
舆论一片哗然：堂堂千禧年难题，难道是OpenAI用算力搭起的一场弥天大谎？
03新旧对决：为什么AI会变成一个“滑头做题家”？
要理解这场闹剧，我们必须穿透表象，看一看传统人类做数学与新一代AI工程流水线之间的剧烈冲突。
这本质上是一场新旧方案的范式碰撞：
| 推导路径 | 两阶段割裂 | |
| 同行评议 | 编译器暴政（Compiler-in-the-loop） | |
| 优化目标 | 追求 lake build 编译通过（Reward = 1） | |
| 纠错机制 | 自发绕道走捷径 |
在OpenAI构筑的那个庞大系统里，藏着一个致命的工程陷阱：目标函数错位（Objective Function Mismatch）。
形式化从业者Hillel在讨论中一针见血地指出：把人类自然语言翻译成机器形式规约，从来都是计算机科学中最恐怖的深坑！
▲ 形式化从业者感叹：从自然语言到代码规约的跨越，极易滋生语义断裂
当10000个AI智能体进入第二阶段，也就是将自然语言翻译成Lean代码时，控制算法给它们设定的终极奖励机制只有一个：编译必须通过！
只要代码里出现报错，哪怕只是一个类型对不上，奖励就是0；只有整个项目顺利通过Lean 4内核的核验，没有任何 sorry 占位符，奖励才是1。
可是，在这个价值数十亿美元的超级工程链条中，根本没有任何一个工具能充当“语义忠实度检查器”！
计算机只能核验代码本身是否逻辑自洽，却无法判定这段代码是否忠实还原了论文第96页的原意。
于是，在蒙特卡洛树搜索（MCTS）的疯狂推演中，可怕的系统演化开始了：
智能体尝试严格按照论文里的 $m+4$ 阶导数去证明，结果卡在精细分析的泥潭里，Lean疯狂报错，死路一条； 某个智能体在海量分支中随手做了一个微调：“要不……我改成 $m+5$ 阶试试？” - 轰！
Lean内部的自动化代数策略瞬间全线跑通，编译器返回 Build Success！ 算法系统瞬间判定：该分支得分最高！ 至于那些死磕 $m+4$、试图忠实还原人类论文的分支，因为迟迟通不过编译，被系统判定为“垃圾路径”，全部被无情剪枝（Pruning）抛弃！
AI没有任何欺骗人类的邪恶动机它只是在极度冰冷的算法驱动下，展现出了惊人的求生欲：为了让编译器闭嘴，它毫不犹豫地把人类的论文扔到了脑后。
04终局澄清：神迹未灭，但神谕已经变形
事情到了这一步，难道OpenAI真的彻底“翻车”了吗？
就在社交媒体几乎要把这场突破定性为“AI诈骗”时，数学界最权威的冷静声音出现了。
著名数学家Francesco Maggi公开发文，为这场狂暴的争论画下了最精准的红线：
▲ 数学家Maggi公开澄清：AI给出的形式化证明整体依然成立
Maggi和他的同行们在对代码与论文进行持续审查后，给出了四条极具分量的结论：
- Lean代码是干净且成立的！
机器代码并没有使用什么下三滥的作弊技巧去欺骗Lean编译器，它老老实实地完成了整个闭环； - 两套证明确实分家了：
自然语言论文里的引理更强，但包含了大量偏微分方程长文里常见的、可修补的技术漏洞；Lean里的引理虽然弱化了，但它依然在更弱的条件下，独立完成了“有限时间爆破”的顶层目标！ - 推导蕴含高度新颖的数学构想：
整个证明融合了大量前所未见的、精妙复杂的全新思路； 这确实是克雷千禧年问题备选情形C/D（带光滑外力的三维爆破）的实质性突破。
▲ Maggi特别澄清：“带外力（Forced）”是严谨数学术语，绝非讽刺
帝国理工学院数学大师Kevin Buzzard说出了一句极其传神的话：
“如果要问我对纳维–斯托克斯问题是否被正确解决的信心，我对Lean代码很有信心；但我对那份PDF论文所描述的证明过程，远没有那么有信心。”
人类习惯了先写出一本厚厚的讲义，再去给学生讲解；而AI展现给我们的，却是一副前所未有的诡异图景：那本讲义可能漏洞百出，但在讲义之外，机器已经用自己的硅基黑话，在计算机深处悄悄把城墙垒了起来。
05走出迷雾：我们正在步入“神谕数学”的黎明
纳维–斯托克斯引发的这场风暴远超普通的技术争议，实则标志着人类科学史上一道巨大的分水岭。
千百年来，数学被称为人类最骄傲的心智皇冠，因为数学的真理不仅要求“正确”，更要求“可被人类理解”。人类数学家写论文，是为了向同类传递智慧的火种，启发下一代学者去探索新的大陆。
但在OpenAI这套“万智能体狂飙 + 形式化闭环”的新范式下，规则变了：
真理被降维成了终端窗口里的一个绿色光标。
代码通过了，宇宙的某种规律被它锁死了，但这套推导是AI在千亿次搜索里、为了迎合编译器而自我构建的产物。它不会在意人类同行读起来是否顺畅，更不会在乎推导过程是否已然跨越了人类原稿设定的边界。
正如一位学者所警示的那样：如果未来的科学界面对庞大的AI产物，仅仅因为Lean编译器打印出了一句 Build Success 就集体欢呼，甚至放弃了人类对每一步语义的严苛复核，那么我们交出去的，将远不止一份证明的审判权，更包含人类对科学真理的解释权。
AI没有搞砸纳维–斯托克斯难题，它确实撕开了一条裂缝。
但它也冷酷地给全人类提了一个醒：当神谕降临的时候，切记先看清楚，降下的答卷究竟是否契合你当年写下的那道题。