24天复核一万五千页：AI智能体蜂群如何破解数学史上最长证明

数学史上最长的一个证明，长达一万五千页。

由上百位顶尖数学家写了整整四十年。

但在过去四十年里，全世界没有一个人能把它完整读完一遍。

连写出它的数学家自己都做不到。

因为实在太长了。

五百多篇论文散落在几十种学术期刊里，堆起来有大半个人高。

哪怕一个数学天才不吃不喝看一辈子，也根本不可能把每一个推理步骤验算完。

但现代数学的绝大多数分支，又天天在心安理得地使用这个定理。

大家其实是在靠一种脆弱的分布式信任硬撑：

我相信你审过的那两百页，你相信他写的那四百页。

所有人心里其实都悬着一把剑：

万一第四千三百页藏着一个隐秘的代数漏洞，上百位学者搭起来的这栋数学摩天大楼，会不会当场塌掉？

这个担忧真不是空穴来风。

早在 1983 年，领头的数学家就曾兴奋地宣布大功告成，结果没过几年就被人发现漏掉了一整个分类分支，最后又花了整整二十年、写了一千多页补丁才勉强合上。

整栋大厦里到底还有没有别的暗雷？

谁都不敢深想，谁也查不清楚。

直到上个月，一群 AI 智能体蜂群扑了上去。

只用了 24 天。

它们把这一万五千页的人类草稿，全部转化成了 4310 万行由机器严密核验的代码。

而且，这群 AI 还真在里面揪出了 34 处人类完全没发现的硬伤。

这个被数学界称为庞大定理的怪物，真名叫有限单群分类定理。

在数学世界里，群论是研究对称性的终极语言，而单群就像是物质世界的原子。

任何一个复杂的有限群，都能像分子拆解成原子一样，被拆成不可再分的单群。

数学家们花了半个世纪，就是想把宇宙中所有可能存在的单群全部找出来，编成一张不会遗漏任何元素的周期表。

最后他们宣布：找齐了，总共四大类，外加 26 个稀奇古怪的散在群。

结论非常优美，但证明过程极其崩溃。

人类数学家写论文，最喜欢在推导中写一句话：显而易见，由引理三可得。

这个显而易见，在人类草稿里往往省略了几十步繁杂的代数推演。

同行审稿的时候，看到作者是数学泰斗，直觉上也合情合理，点点头就放行了。

这就是为什么过去没人敢验算整部定理：

人类的肉脑根本容纳不下一万五千页里环环相扣的细节。

那为什么以前的大模型干不了这事？

因为大模型靠概率预测下一个词，最擅长一本正经地胡说八道。

数学容不得半点玄学，推导漏了一环，整条链条全部归零。

这次做出突破的 Axiom 团队，做法截然不同：

大模型不当裁判，它只负责给一个冷酷的编译器打工。

这个编译器叫 Lean 4，是一门严苛的形式化数学验证语言。

在 Lean 4 的世界里，没有任何显而易见。

所有的公理、定义和推理，都必须写成严丝合缝的代码。

只要逻辑中间漏掉一个假设，或者推导跳跃了一小步，编译器当场报错，绝对不给通过。

面对五百多篇人类论文，Axiom 的智能体蜂群是怎么啃下来的？

第一步是拆解依赖图谱。

总控智能体把一万五千页的论文切成两百多万个独立的数学命题和引理，拉出一张庞大的有向无环图。

哪一个结论支撑哪一个推论，全部分解成树状结构。

第二步是分布式代码化与证明搜索。

成群结队的专业智能体被分配到图谱的每一个细小节点上。

它们负责把人类的自然语言翻译成代码，并尝试写出形式化证明。

证明卡住了，智能体就根据编译器的报错反馈，自主回溯并寻找新的路径；

推导成功了，这段代码就变成一块绝对坚实的积木，提供给上游的智能体继续使用。

人类审稿会累、会轻信权威、会产生直觉盲区，但机器编译器不会。

当这套系统扫到非平衡群定理时，警报响了。

这是整个分类工程里的一大核心支柱。

1986 年数学家约翰·沃尔特（John Walter）发表过一篇关键论文，里面有一步关于集合闭包的断言，被学术界引用了整整四十年。

几十年来，无数顶尖学者读到那里时都觉得理所当然。

但这次，AI 无论如何都无法在 Lean 4 里把这一步推导闭合。

深入排查之后才发现，沃尔特当年那一步推论其实藏着反例，在逻辑上根本推导不出来。

那是一个潜伏在数学文献里四十年的真正漏洞。

发现断裂后，AI 蜂群没有停下，直接联合研究团队调换路线，顺着 1976 年另一位数学家所罗门（Ronald Solomon）给出的方法重新布局，硬是用机器生成的新证明把这个四十年的大坑彻底补齐。

整整 4310 万行 Lean 4 代码，完成了 108 个核心验证节点。

没有任何一行代码是人类敲进去的，全部由机器生成，并且每一行都通过了编译器的逻辑核验。

人类花了四十年、上百位数学家的青春才勉强拼凑起来的宏伟拼图，被 AI 蜂群在 24 天里全部复查并加固完毕。

以前大家总以为科学探索最缺的是天才灵感，

但现实告诉我们，很多时候阻碍科学前行的，只是人类大脑狭窄的验证带宽。

当不知疲倦的智能体蜂群遇上六亲不认的严谨编译器，科学史上那些因篇幅过于庞大而无法查验的灰色地带，第一次有了被彻底照亮的可能。