AI 用 24 天让计算机核对完数学史上最长的证明：定理成立，但其中一篇论文的证法有漏洞，AI 换了一种证法补上

一个证明长达 1.5 万页，散落在 500 多篇论文里，几十年来没有一个人从头到尾读完过，它到底对不对？AI 数学公司 Axiom 10 月 26 日宣布，他们用几十个 AI agent 花了 24 天，把这个证明全部改写成计算机能逐步检查的代码，Axiom 说检查已经全部通过。

这个证明对应的是“有限单群分类定理”，外号“巨大定理”，约 100 位数学家花了几十年才完成。

【这个定理讲什么】

先说“群”。一个立方体，你能找到 24 种转法，转完它看起来跟没动过一样。数学家把这样一组“转完看起来不变的操作”叫做一个群，它是研究对称的工具。

整数可以拆成质数相乘，质数再也拆不动。群也一样，可以拆成一些拆不动的基本单位，叫“单群”。有限单群分类定理给出了一张完整清单：所有基本单位，要么属于几个有固定规律的大家族，要么是 26 个不属于任何家族的特例。最大的特例叫“魔群”，元素个数是 8 后面跟 53 个零。

找到这些单群不算最难，难的是证明清单里没有漏掉任何一个。

【为什么要计算机来查】

证明太长，人查不过来，出过错也不奇怪。1983 年，牵头的数学家宣布证明完成，后来发现其中一块根本没写完，直到 2004 年才用一本 1221 页的书补上。

Axiom 用的检查工具叫 Lean。把证明翻译成 Lean 能读的代码后，它会一步一步核对：每一步是不是真的能从前面推出来。人读论文时会默认“这步显然成立”，Lean 不接受，必须写出来。2012 年有团队用类似工具，花了约 6 年才查完这个定理里一篇 255 页的论文。

【查出了什么】

先说结论：定理本身没错，清单还是那张清单。

问题出在中间一篇论文的证法上。整个证明要用到一个叫“不平衡群定理”的中间结论，Axiom 照着数学家 John Walter 1986 年给出的证明来翻译，AI 发现这个证明里引用的一个说法是错的，并举出了具体的反例。好比一道几何题，答案是对的，但书上的解法中间用了一个不成立的条件，解法得换。

Axiom 请教了当年参与原始证明的数学家 Richard Lyons 和 Ronald Solomon，借用 Solomon 1976 年的一套思路，由 Axiom 的 AI 写出一个新证法，绕开了出错的那一步，也通过了 Lean 的检查。新证法已经整理成一篇 35 页的论文。

除此之外，查出来的大多是笔误、表格写错、少写了前提这类小毛病。Axiom 博客说其中 34 处值得专门处理，完整清单还没公布。Axiom 的推文说法更重，称修了“几百处重大勘误”。

【AI 怎么干的】

几十个 AI agent 分工：有的把大的论证拆成小定理，有的去找已有结果，有的写 Lean 代码。人类数学家处理 AI 卡住的数学难题，工程师维护系统。最后写出约 4310 万行代码（推文说约 5000 万行，博客和官网都是 4310 万），其中约 120 万行来自清华大学求真书院团队此前开源的同类项目。

AI 有时会把还没证明的东西直接当成已知条件用，Axiom 发现后删掉了几万行代码重来。用的是哪些 AI 模型，Axiom 没说。

【能全信吗】

Lean 能保证推导的每一步都对，但它判断不了代码开头写的那句“定理”是不是真的就是有限单群分类定理。如果这句话翻译走了样，后面证得再对，证的也是另一件事。这部分只能靠人读。Axiom 邀请群论学家和 Lean 社区自己重跑检查、核对这句话。目前这还是 Axiom 自己的发布，还没有外部独立核查的结果。

Axiom 博客：https://axiommath.ai/research/the-enormous-theorem-formalized/
项目网站：https://cfsg.axiommath.ai/
Axiom 推文：https://x.com/axiommathai/status/2115089794867040584