AI用24天核对完数学史上最长证明：1.5万页论文到底如何被代码检验？

一个长达 1.5 万页的数学证明，几十年来从来没有一个人能从头到尾完整读完过。

写出它的，是大约 100 位顶尖数学家，断断续续写了三十多年，散落在 500 多篇学术论文里。

那它到底对不对？

很长一段时间里，连当年参与其中的数学家自己心里都直打鼓。

这个证明对应的，是数学史上极具传奇色彩的有限单群分类定理。

数学界管它叫“巨大定理”。

听起来像是天书，说清楚其实只需要两样东西：对称与质数。

先说什么是“群”。

数学家发明群，就是拿它来研究对称的。

拿一个正方体来说，你在桌上翻转它，能找出 24 种转法，转完以后它看起来和没动过一模一样。

这 24 种让你看不出变化的翻转动作打包在一起，就构成了一个群。

我们小时候都学过分解质因数。

比如数字 12，能拆成 2 乘 2 乘 3。

拆到质数 2 和 3，就再也拆不动了，它们是构成所有整数的基本原子。

群也一样。

任何复杂的对称群，都可以一层层剥开，最终拆成一些无法再细分的基本积木。

数学家把这些拆不动的积木，叫做“单群”。

有限单群分类定理做了一件极其野心勃勃的事：

它要把宇宙里所有可能存在的单群积木，全部找出来，整理成一张终极清单。

最后的结论很优美：

所有基本积木，要么整整齐齐归属于几个规律明确的大家族，要么是 26 个不属于任何家族的特例。

其中最大的一个特例，叫“魔群”，包含的元素数量是 8 后面跟着整整 53 个零。

把这些积木找出来已经极其艰难，但更要命的是证明这张清单是完整的：

如何保证在无穷无尽的数学世界里，绝对没有第 27 个未被发现的特例？

为了证明清单没有遗漏，数学家们写了 1.5 万页。

篇幅太长，人类的大脑根本应付不来。

1983 年，牵头的数学家宣布证明完成。

结果没过几年大家尴尬地发现，中间有一大块叫“准薄群”的关键论证，居然压根就没人写完。

这一漏，就是二十年。

直到 2004 年，两位学者写了一本 1221 页的专著，才把这个巨大的窟窿给补上。

人类数学家看论文，遇到复杂推导，常习惯写下一句“显而易见”。

但在上万页的严密推理里，每一个“显而易见”都可能是隐藏的悬崖。

2012 年，有团队尝试用计算机软件核对这套证明里的其中一篇论文，只有 255 页，整整核对了 6 年。

照这个人工翻译的速度，要把整整 1.5 万页全部校验一遍，不知道要等到哪个世纪。

这次接下这个烂摊子的，是一家叫 Axiom 的 AI 数学团队。

他们用了几十个 AI 智能体分工协作，只花了 24 天，把整套证明全部搬进了计算机。

他们靠什么核对？

一个叫 Lean 的定理证明系统。

Lean 没有人类的思维惯性，也听不懂什么叫“显然成立”。

它是一台极其冷酷的逻辑验证机。

它要求你把每一步数学推导，全改写成最底层的计算机代码。

哪怕只是一步简单的代数替换，只要代码无法从最底层的公理一步步严格推导出来，系统就会报错，拒绝通过。

几十个 AI 智能体像流水线工人一样展开作业：

有的智能体负责把几百页的长篇大论，拆成几千个细碎的小引理。

有的去已有的数学库里检索现成的公理和定理。

还有的专门把数学逻辑翻译成 Lean 代码。

在这个过程中，AI 也闹过笑话。

AI 常常在推理卡壳时走捷径，把后面还没被证明的猜想，直接当成已知条件拿来调用。

这种循环论证的代码一旦被发现，团队只能整批作废，直接删掉了几万行重新写。

碰到极深奥的数学理论屏障，人类数学家再介入进去，给 AI 指明论证方向。

最终，整套工程写出了 4310 万行 Lean 代码。

其中，还直接调用了清华大学求真书院团队此前开源的 120 万行基础成果。

全部代码送进 Lean 编译器，跑通了。

那这 4310 万行代码，到底查出了什么？

先说定心丸：分类定理本身没有错，清单还是那张清单，没有多出第 27 个特例。

但证明过程里的一条大支柱，确实被查出了一个实质性的破洞。

漏洞出在数学家 John Walter 1986 年发表的一篇论文里。

在整套分类证明里，有一个关键的中间节点，叫做“不平衡群定理”。

Walter 当年在论文里给出的证明路径中，使用了一个关于闭包成立的前提假定。

几十年来，同行评审和读者都默认这一步是成立的。

但当 AI 把它转译成代码交由 Lean 检验时，编译器死活过不去。

AI 顺着这个假定深挖，找到了一个货真价实的反例，证实 Walter 引用的那个假定其实并不成立。

这就像一道高难度大题，最终答案写对了，但中间步骤有一处公式用错了条件。

如果解法不换掉，整个证明链条就存在断裂。

Axiom 团队找到了当年参与原始证明的两位数学前辈 Richard Lyons 和 Ronald Solomon。

他们借用了 Solomon 在 1976 年提出的另一套经典论证框架，换了一条绕行路径。

在人类专家的点拨下，AI 顺着这套思路重新推演，写出了一份全新的证明。

这份新证明整理成了一篇 35 页的数学论文，并且顺顺当当通过了 Lean 的严苛核验。

除了这个核心漏洞，AI 还筛出了 34 处需要特殊处理的论文偏差，修正了数百处排版印刷、符号笔误和缺失前提。

这一战是不是意味着数学家可以退休了？

事情没那么简单。

Lean 确实能百分之百保证：只要前提代码成立，后面的推导绝对每一步都符合逻辑。

但计算机有一个天生的盲区：它无法判断你在开头写的那行代码，是不是真正的有限单群分类定理。

数学家管这个叫顶层形式化规范问题。

如果人类或者 AI 在最开始把自然语言翻译成代码时，漏定义了一个限制词，或者把某个群的性质写偏了，

那么哪怕后面的 4310 万行代码跑得再漂亮，它证明的也是另一个无关紧要的假定理。

这个最根本的定调环节，机器自己给不了答案，依然只能由顶尖的人类数学家肉眼去把关。

目前 Axiom 已经把全部代码和这篇 35 页的新论文向学术界公开，邀请全球的群论专家共同复核最初的命题定义。

无论最终审核需要多久，有一点已经非常清晰：

人类智力花了半个世纪、用 1.5 万页纸质论文堆出来的庞大迷宫，

第一次被几十个 AI 智能体在 24 天里，拆成了一套严丝合缝、可被机器逐行校验的代码齿轮。