数十agent，24天挑战数学界巨型工程，还揪出40年前漏洞

数十个AI智能体，耗时24天挑战数学界巨型工程，还发现了40年前的论证漏洞。

超过100位顶尖数学家，投入数十年时间，撰写了1.5万页的证明。

如今，人工智能仅用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的，36氪经授权发布。