100 多位顶尖数学家，耗费数十年，写下 1.5 万页证明。

现在，AI 只用了 24 天，就把这项人类数学史上最庞大的工程之一，变成了 4300 多万行可以由计算机逐步验证的代码。

更惊人的是，AI 在检查这些数学家留下的证明时，还揪出了一个存在近 40 年的论证漏洞。

这不是一道奥数题，也不是一篇几十页的数学论文，而是被称为「巨型定理」（Enormous Theorem）的有限单群分类定理。

从 20 世纪中叶开始，上百位数学家参与了这场研究。1983 年，数学家 Daniel Gorenstein 宣布分类工作已经完成，但此后人们发现其中仍有未补齐的部分。直到 2004 年，数学家又用 1221 页证明填上了一个关键缺口。

10 月 26 日，AI 数学公司 Axiom Math 宣布，由人类数学家和工程师组织的数十个 AI Agent，在 24 天内完成了这一巨型定理的 Lean 形式化，生成约 4310 万行代码、205 万个形式化声明，给出了第一份覆盖整个分类定理的计算机检查证明。

原本分散在 500 多篇论文中的数学推理，如今被组织成一套能够逐步检查的形式系统。更让人意外的是，在这个过程中，Agent 不仅找出历史论文里的错误，还参与构造了一项新的群论结果。

Axiom 公开的有限单群分类定理形式化项目，包含约 4310 万行 Lean 代码、205 万个声明、100 个里程碑，涉及 715 篇参考文献。图源：Axiom Math 官网。

数学界花了数十年，究竟在证明什么？

理解这项工作的难度，要从「对称性」说起。

一张正方形纸片，旋转 90 度后，形状与原来完全重合；旋转 180 度、270 度也是如此。数学家把这些旋转操作及其组合构成的结构称为「群」。从几何图形到粒子物理，群论提供了一种研究对称性的通用语言。

复杂的有限群，可以在一定意义上分解为更基本的部分。就像整数能分解为质因数，这些不能继续拆分的「基本粒子」被称为有限单群。

有限单群分类定理要回答一个看似朴素的问题：所有这样的基本粒子，到底有哪些？

最终清单包含素数阶循环群、交错群、16 个无穷系列的李型单群，以及 26 个特殊的「散在单群」。其中最大的「魔群」（Monster Group），拥有约 8×10^53 个元素。光是证明它存在，就曾是数学界的一项重大成就。

部分「散在单群」之间的关系示意图。其中，顶部的 M 代表最大的散在单群「魔群」（Monster Group），其他节点代表不同的散在单群。

找出这些群，只完成了一半工作。真正难的是证明：除了清单里的类型，不可能再有第 27 个散在单群，也不存在任何尚未发现的新类型。

1963 年，Walter Feit 和 John Thompson 用 255 页论文证明，所有非交换有限单群的阶都是偶数，为后续分类打开了突破口。1972 年，Gorenstein 提出 16 步研究计划；1983 年，他宣布分类完成。后来留下的拟薄群证明缺口直到 2004 年才由 Michael Aschbacher 和 Stephen Smith 补齐，2008 年又出现进一步修正。

庞大的证明像一张跨越数十年的关系网：某篇论文引用另一篇的定理，后者又依赖更早的引理。许多步骤还省略了作者认为显而易见的条件。即使每篇论文单独看起来合理，也很难由一个人检查整套体系的每一处连接。

Axiom 这次要做的，就是把这些连接全部转化成计算机能够核查的证明。

24 天的 Agent 工程，差点被「正确的证明」拖垮

这不是让一个大模型读完 1.5 万页，再一次性吐出几千万行代码。

10 月 1 日，Axiom 开设专门的 Slack 频道，利用已有的 Lean 基础库和数学文献，整理出一张证明路线图：108 个里程碑、约 380 项具体任务。10 月 2 日，第一批 Agent 开始通过 GitHub Issues 认领任务。

有的 Agent 负责拆解定理，有的搜索已有结果，有的生成 Lean 证明，还有的审查命题、整合代码。遇到尚未完成的前置定理，Agent 可以继续将任务交给其他 Agent。人类数学家处理关键障碍，工程师则负责协调这些持续工作的系统。

这些 Agent 由 Axiom 自主开发的数学证明系统 AxiomProver 协调运行。项目采用了不断调整的多模型组合，但没有公开具体的底层模型名单。相比依靠单个模型完成推理，这套系统更强调不同 Agent 之间的任务拆解、证明生成和协作验证。

Axiom 有限单群分类定理形式化工程的矩形树图（Treemap），展示了不同数学模块中的 Lean 声明与代码规模。图源：Axiom Math。

开工后不久，一个棘手问题出现了：Agent 能够证明一条数学命题，却未必证明了项目真正需要的那一条。

比如，原本要求证明一座桥能让重型卡车安全通过，Agent 却先增加了一个条件：「假设桥墩足够坚固」。有了这个前提，它顺利证明了卡车可以通过，甚至连 Lean 都认可整个推导。

但问题是，桥墩究竟够不够坚固，根本没有得到证明。

类似的问题在项目早期反复出现。一些看似已经完成的数学任务，实际上悄悄引入了尚未证明的前提。Axiom 不得不删除数万行建立在这些假设之上的代码，重新安排工作。

随着代码库膨胀，Lean 的检查速度也开始跟不上 Agent 产出。修改一条基础定理，可能迫使所有依赖它的代码重新检查。工程师为此引入共享构建缓存和并行验证机制，让不同 Agent 尽量复用已经确认的结果。

10 月 10 日，团队 Slack 频道里传来好消息：「WE PROVED MONSTER IS SIMPLE.」Agent 已经完成了魔群单性的形式化，还通过 Griess 代数形式化了它的存在性。

但三天之后，项目进度突然慢了下来。10 月 13 日，尽管数十个 Agent 还在不停生成代码，团队一整天却只完成了一个阶段性证明任务。

问题出在任务拆分上。剩下的数学难题太过复杂，一道大题下面还藏着许多尚未解决的小问题。Agent 虽然能不断写出新的证明，却很难判断究竟解决了多少关键步骤，距离最终目标还有多远。

Axiom 不得不重新调整策略，把复杂的证明拆成更小、更明确的任务，并要求 Agent 说明这些小证明如何一步步组合起来，最终得到原本需要的结论。

AI 翻出 40 年前的旧账，还补出一条新证明

当证明进入历史文献最深处，Agent 发现了比任务调度更麻烦的事情：原来的数学论文也可能写错。

人类数学家常常省略熟悉的推理，但 Lean 要求明确写出每个前提。Axiom 统计，形式化过程中有 34 处值得关注的文献偏差需要处理，其中既有笔误、遗漏条件，也有必须重新推导的实质性问题。

一个例子出现在 Aschbacher 和 Smith 研究「拟薄群」的著作中。原文的一条引理断言两个量相等，Agent 却借助群 SL₂(5)找到反例：一个量是 1，而等式要求它是 2。把等式改成不等式，可以修正引理，但后面的推理曾依赖那个等号。团队只得扩大前面一段论证的适用范围，重新处理受影响的情况。

更大的障碍来自 1986 年 John Walter 关于「不平衡群定理」（Unbalanced Group Theorem，UGT）的研究。

UGT 是有限单群分类的重要工具。它帮助数学家利用一个群内部的特定局部结构，推断整个群可能属于什么类型。Walter 的一条关键推理默认：对特定群族进行某种操作，得到的相关单群仍属于原来的群族。

Agent 找到了反例。以 PSL₂(49)为起点，考虑其有限域自同构所诱导的对合，相关中心化子的单群成分会出现 PSL₂(7)。但后者恰好不属于 Walter 限定的群族，原来的闭包断言无法成立。

这并没有推翻 UGT 的结论，却意味着沿用这条证明路线时，有一步必须另找依据。

Axiom 为此咨询了群论专家 Richard Lyons 和 Ronald Solomon。Solomon 在 1976 年提出的极大 2-分量理论，为新路线提供了关键思路。

Agent 随后构造并形式化了一项新的群论结果「Preservation of simple tops」，证明在所需条件下，比较特定子群时能够保留相关单群结构。它被写入一篇 35 页的《The Unbalanced Group Theorem》论文，作为定理 2.3，并与其他已有结果组合，完成了分类所需的 UGT 证明。

有意思的是，形式化结束后，Axiom 的数学家又在第一代证明方法中发现了更短的路径，无需调用这条新定理也能得到目标结论。不过，新定理及其完整证明仍被保留下来，成为这场工程额外产生的数学成果。

Axiom 团队参与完成的不平衡群定理研究，其中定理 2.3「Preservation of simple tops」是此次形式化过程中得到的新数学结果。图源：论文《The Unbalanced Group Theorem》。

4310 万行 Lean 之后，数学证明发生了什么变化？

最终，Axiom 将整个项目上传 GitHub，公开了约 4310 万行 Lean 代码。仓库中的最终分类命题，表达的是：每一个有限单群，都与清单中某个已经构造出的群同构。

项目声明最终证明不含 sorry——在 Lean 里，它是暂时跳过未完成证明的占位符。最终结果只依赖标准公理，并可由 Lean 内核逐步检查。Axiom 同时提供了交互式证明依赖图，让研究者追踪一个结论究竟依靠哪些前置定理。

Axiom 公开的有限单群分类定理最终 Lean 代码。最终结论通过调用已经形式化的底层证明得到，背后是数千万行 Lean 代码构成的证明工程。图源：Axiom Math / GitHub。

这项工作的基础也包括 Mathlib、TauCeti 和 Qiuzhen-CFSG 等已有形式化项目，其中约 120 万行来自 Qiuzhen-CFSG。人类数学家积累的研究成果、早期形式化基础设施，以及可以并行工作的 AI Agent，被放进了同一套工程流程。

对后续数学研究而言，一项关键改变是证明可以被持续维护。过去引用有限单群分类定理，背后可能牵连数百篇文献；现在，研究者可以沿着形式化的依赖链，检查具体使用了哪些定义、条件和推导。

Axiom 公开的仓库将审查状态标为团队自评。接下来，外部数学家仍可以检查形式化定义是否准确对应原命题，并审阅这项庞大工程中的数学选择。但 Lean 已经提供了另一种此前难以获得的能力：让数千万行证明的逻辑推导接受统一、机械化的检查。

回看这 24 天，最值得关注的并非 AI 写出了多长的代码，而是它开始处理一项过去高度依赖人类专家的大规模研究工作：拆解任务、追踪证明、发现旧文献中的错误，并在旧路线走不通时参与构造新证明。

数十年积累起来的数学知识，正在从散落在论文中的论证，变成可以被程序检查、复用和继续扩展的结构。Axiom 这次展示的，正是 AI 从解答单道数学题，走向参与整套数学理论建设的一次具体尝试。

本文来自微信公众号 “机器之心”（ID：almosthuman2014），作者：关注AI的