AI用24天形式化巨型定理，还揪出40年前漏洞

100多位顶尖数学家耗费数十年、写下1.5万页证明的有限单群分类定理，如今被AI在24天内转化为约4310万行可由计算机逐步验证的Lean代码，并揪出一个存在近40年的论证漏洞。

有限单群分类定理被称为“巨型定理”。从20世纪中叶起，上百位数学家参与研究。1983年，Daniel Gorenstein宣布分类完成，但此后发现仍有未补齐部分。2004年，数学家又用1221页证明填上关键缺口。最终清单包含素数阶循环群、交错群、16个无穷系列的李型单群，以及26个散在单群，其中最大的“魔群”拥有约8×10^53个元素。证明的核心难点在于：除清单所列类型外，不可能再有新的散在单群或尚未发现的新类型。

10月26日，AI数学公司Axiom Math宣布，由人类数学家和工程师组织的数十个AI Agent，在24天内完成该定理的Lean形式化，生成约4310万行代码、205万个形式化声明，给出第一份覆盖整个分类定理的计算机检查证明。项目涉及715篇参考文献、100个里程碑。原本分散在500多篇论文中的推理，被组织成可逐步检查的形式系统。

工程并非让单个大模型一次性生成代码。团队先整理出108个里程碑、约380项任务的路线图，由不同Agent分别负责拆解定理、搜索已有结果、生成Lean证明、审查命题和整合代码，人类数学家处理关键障碍。项目由Axiom自主开发的AxiomProver协调运行，采用多模型组合，但未公开底层模型名单。

过程中出现两类问题。其一，Agent能证明一条命题，却未必是项目真正需要的命题，常悄悄引入未证明前提，团队不得不删除数万行代码重做。其二，任务拆分过粗导致进度停滞，后改为更小、更明确的任务并要求说明组合方式。此外，Lean检查速度一度跟不上Agent产出，工程师引入共享构建缓存和并行验证机制。

在核查历史文献时，Agent发现34处值得关注的偏差。一例出现在Aschbacher和Smith关于“拟薄群”的著作中，原文一条引理断言两个量相等，Agent借助群SL₂(5)找到反例，将等式改为不等式并重新处理受影响推理。更大的障碍来自1986年John Walter关于“不平衡群定理”（UGT）的研究：其关键推理默认对特定群族进行某种操作后相关单群仍属原群族，Agent以PSL₂(49)为起点找到反例，相关中心化子的单群成分出现PSL₂(7)，而后者不属于Walter限定的群族。这并未推翻UGT结论，但意味着沿用原路线时有一步必须另找依据。

Axiom为此咨询群论专家Richard Lyons和Ronald Solomon。Solomon 1976年提出的极大2-分量理论为新路线提供思路。Agent随后构造并形式化新结果“Preservation of simple tops”，证明在所需条件下比较特定子群时能保留相关单群结构，作为定理2.3写入35页论文《The Unbalanced Group Theorem》，并与其他结果组合完成UGT证明。形式化结束后，数学家又在第一代证明方法中发现更短路径，无需调用该新定理也能得到目标结论，但新定理及完整证明仍被保留。

最终，Axiom将项目上传GitHub，公开约4310万行Lean代码。仓库中的最终分类命题表达为：每一个有限单群，都与清单中某个已经构造出的群同构。项目声明最终证明不含sorry占位符，只依赖标准公理，并可由Lean内核逐步检查。Axiom同时提供交互式证明依赖图，供研究者追踪。