Axiom Math 发布群分类定理的 Lean 证明，含 4310 万行代码

Axiom Math 于 2026 年 10 月 27 日表示，公司将发布其称为首个经计算机完整校验的有限单群分类定理证明。工程师和数学家指挥数十个 AI 智能体组成的集群，在 24 天内完成了这一成果；这些智能体在 Lean 证明助手中编写了约 4310 万行代码。

公司在公告中写道：“今天，我们发布了首个经计算机完整校验的有限单群分类定理（CFSG）证明。”该分类定理确定了有限群的基本构件。其原始证明分布在 500 多篇论文中，篇幅约 1.5 万页，约有 100 位数学家参与撰写；如此浩大的规模使它获得了“巨大定理”的绰号。

Axiom 发布了什么

CFSG 确立了这样一条结论：每个有限单群都属于以下情况之一：素数阶循环群；作用于至少五个符号上的交错群；在有限域上构造的 16 个李型群无限族之一；或恰好 26 个孤立的散在群之一。公告指出，有些作者将蒂茨群计作第 27 个散在群。最大的散在群——魔群——由 Robert Griess 于 1980 年利用一个维数为 196,884 的代数构造而成。

人类证明这一分类定理的工作历经数十年。1963 年，Walter Feit 和 John Thompson 在一篇长达 255 页的论文中证明，每个非阿贝尔有限单群的阶都是偶数；这篇论文占满了整期《Pacific Journal of Mathematics》。Daniel Gorenstein 于 1972 年提出了一个包含 16 个步骤的计划，以完成这一分类，并在 1983 年宣布分类工作已经完成。然而，拟薄情形当时仍依赖 Geoffrey Mason 尚未完成的手稿，直到 Michael Aschbacher 和 Stephen Smith 于 2004 年发表一篇长达 1,221 页的论述，才补上这一部分，完成后来被称为第一代证明的工作。Gorenstein 和 Richard Lyons 开始构建一套更系统的第二代证明，Ronald Solomon 和 Inna Capdeboscq 后来也加入其中；这项工作至今仍未完成，因此 Axiom 将第一代证明形式化。

项目页面介绍称，这项形式化工作遵循第一代证明，并由 Lean 内核检查每一个逻辑步骤；页面还列出了 4310 万行 Lean 代码、205 万条声明，以及其语料库收录的 715 篇论文和书籍。Axiom 表示，其证明路线图参考了第二代证明系列著作；这项形式化工作还纳入了早期 Qiuzhen-CFSG 项目约 120 万行代码，并以 Mathlib 为基础。Axiom 将 Mathlib 的开发归功于数百位贡献者。项目页面列出的核心贡献者包括 Dean Cureton、Vasily Ilin、Bhavik Mehta 和 Niels Voss，首席研究员为 Letong Hong。

公开的 GitHub 代码库将这一成果描述为一项不含 sorry 占位符的 Lean4 证明，固定使用 4.35.0-rc3 版本，以 Mathlib 和 TauCeti 项目为基础，仅使用标准公理 Classical.choice、propext 和 Quot.sound，不使用 native_decide。该分类定理的形式化陈述取自 TauCeti，内容如下：“每个有限单群都同构于分类列表中某个经过明确构造的群。”README 指出，lake build 会检查整个开发成果；对 Lake 构建工具的开放式修改，以及团队计划向上游提交的优化，将构建时间缩短至 24 小时以内。代码采用 Apache-2.0 许可证。

历时 24 天的智能体集群协作

2026 年 10 月 1 日，Axiom 开设了一个 Slack 频道，以协调该项目。团队利用此前已有的 Lean 工作，以及根据已发表文献整理出的内部证明路线图，将工作划分为 108 个里程碑和约 380 项较小任务。首批智能体于 2026 年 10 月 2 日开始运行，通过 GitHub issues 认领里程碑，并在 Slack 中报告已完成的工作。主导智能体负责拆解困难论证并审查命题；其他智能体则搜索已有结果或编写 Lean 证明。智能体还可以将缺失的前置证明委派给其他智能体，其成果随后会进入共享代码库。

早期进展暴露出一些薄弱环节。有些看似容易处理的里程碑实际上依赖大量前置条件，而智能体只是默认这些条件成立，并未加以证明。团队因此删除了数万行建立在这些假设之上的代码，随后重新制定了更为严谨的计划。早期的一个里程碑涉及信号子函子定理，其候选证明依赖尚待论证的结构性假设。随着智能体生成证明的速度超过 Lean 重新检查证明的速度，构建时间也成了瓶颈。Axiom 表示，工程师将缓存的构建结果分发给各个工作节点、并行运行独立检查，并将耗时的有限计算移至外部执行，再生成可单独检查的证书。公司称，这些改动将验证速度提升了数个数量级。

Axiom 称，2026 年 10 月 10 日，频道中有人发消息宣布智能体已证明魔群是单群。公司还表示，智能体通过 Griess 代数将魔群的存在性形式化，并证明了一个将魔型群与魔群等同起来的定理。2026 年 10 月 13 日，团队只完成了一个里程碑；工程师随后启动重新规划，将尚未完成的里程碑拆分为更小、表述精确的定理。每次拆分都必须通过一个简短的 Lean 证明，说明这些部分如何共同推出原来的里程碑。

在已发表的证明中发现缺漏

Axiom称，将证明转写为 Lean 代码的过程中，团队发现已发表论证中存在问题。大多数问题较小，例如排版错误、表格错误或遗漏假设；但据该公司统计，与已发表版本相比，有34处值得注意的出入，其中最重大的一处涉及《The Unbalanced Group Theorem》（简称 UGT）。

其中一个例子出现在 Aschbacher 和 Smith 的准薄群专著中：一条引理断言两个数值相等。智能体发现了一个涉及群 SL₂(5) 的反例，其中一个数值为1，而断言的等式要求它等于2。将等式改为不等式后，引理便得到修正；但后续论证曾利用等式排除某些情形，因此团队扩展了先前的一项论证，以涵盖这些构型。

UGT 有助于根据子群的信息识别整个群：根据配套论文的摘要，在分类问题的归纳假设下，若一个非平凡奇数阶子群正规地包含于某个对合元的中心化子中，那么所在的单群必为奇特征的李型群，或某些次数的交错群。Axiom 通过 John Walter 1986 年的专著研究 UGT；在形式化这一论证时，其智能体发现，该论证所用的一条闭包断言存在明确反例：一种被认为能使相关单群继续属于指定族的运算，可能会产生一个明确不属于该族的群。

据该公司介绍，从 PSL₂(49) 出发，其域自同构的中心化子为 PGL₂(7)，而这一运算会得到单群 PSL₂(7)。由于7是梅森素数，PSL₂(7) 不属于该群族。Axiom 指出，这些反例并未推翻 UGT 本身，甚至没有推翻 Walter 命题 II.5.9(ii) 的结论。

这一修正借鉴了 Solomon 1976 年提出的极大 2-分量理论。Axiom 称，该理论为其 AxiomProver 系统生成并形式化的一种替代论证提供了核心思路。论文将关键步骤表述为定理 2.3（简单顶端的保持）；Axiom 称，这是由 AxiomProver 证明的群论新结果。结合 Gilman 和 Solomon 的约化结果，以及 Foote 和 Harris 的识别定理，该结果给出了分类所需的 UGT 的单群形式。形式化完成后，Axiom 的数学家在第一代方法的框架内找到了一个更简短的推导，记录于备注 9.5；该推导无需使用定理 2.3，也能得出相同结论。

这篇论文《The Unbalanced Group Theorem》由 Colin Defant 和 Ken Ono 撰写，于2026年10月27日以第1版形式发布在 Hexagon 预印本服务器上，采用 CC BY 4.0 许可协议；项目页面标注论文共35页。Axiom 表示，正在与群论学家合作，汇总文献中发现的勘误，并将在项目的勘误页面上公布。分类理论以 Lyons 和 Solomon 的工作为基础；两人曾就 UGT 的修正提供意见。该公司表示，将继续在包括他们在内的顾问委员会协助下整理并解决这些勘误，同时也有外部顾问 Dan Nakano 参与。Axiom 将自身贡献概括为：使证明能够通过机器核验，记录遇到的障碍，并提供解决这些障碍的形式化论证；同时强调，发现这些群并发展相关论证的数学家，才是完成这项分类工作的功臣。