Axiom Math 发布 4310 万行 Lean 有限单群分类形式化证明

Axiom Math 于 2026 年 10 月 27 日表示，它正在发布其所谓的首个完整计算机检验的有限单群分类证明。该证明由工程师和数学家指挥数十个 AI 智能体组成的集群，在 24 天内完成，在 Lean 证明助手中编写了约 4310 万行代码。

“今天，我们发布首个完整计算机检验的有限单群分类（CFSG）证明，”该公司在公告中写道。该分类确定了有限群的基本构建块，其原始证明横跨约 100 位数学家的 500 多篇文章、约 15000 页，这一规模使其获得了“巨大定理”的绰号。

Axiom 发布了什么

CFSG 确立：每个有限单群要么是素数阶循环群，要么是至少五个符号上的交错群，要么是在有限域上构造的十六个李型群无限族之一，要么是恰好 26 个孤立散在群之一；公告指出，一些作者将 Tits 群计为第 27 个。最大的散在群 Monster 由 Robert Griess 于 1980 年使用一个维数为 196,884 的代数构造而成。

人类证明工作跨越了数十年。1963 年，Walter Feit 和 John Thompson 在一篇 255 页、占满整期《太平洋数学杂志》的论文中证明：每个非阿贝尔有限单群都具有偶数阶。Daniel Gorenstein 于 1972 年提出了完成分类的十六步计划，并于 1983 年宣布其完成，但 quasithin 情形依赖于 Geoffrey Mason 一份未完成的手稿，直到 Michael Aschbacher 和 Stephen Smith 于 2004 年发表了 1221 页的处理，才补上了后来被称为第一代证明的缺口。由 Gorenstein 和 Richard Lyons 开始、后来 Ronald Solomon 和 Inna Capdeboscq 加入的更为系统的第二代证明仍未完成，因此 Axiom 形式化了第一代证明。

项目页面称，该形式化遵循第一代证明，每个逻辑步骤都由 Lean 内核检查，并列出 4310 万行 Lean、205 万条声明，以及语料库中的 715 篇论文和书籍。Axiom 表示，其证明地图借鉴了第二代卷册，并且该形式化纳入了早期求真-CFSG 项目约 120 万行代码，并建立在 Mathlib 之上，该公司将 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 issue 认领里程碑，并在 Slack 中报告已完成的工作。主导智能体分解困难论证并审查陈述，其他智能体则搜索已有结果或编写 Lean 证明，一个智能体可以将缺失的前提条件委托给其他智能体，其结果进入共享仓库。

早期进展暴露了薄弱点。一些看似可管理的里程碑隐藏着巨大的前提条件，智能体只是假设而非证明，团队删除了建立在这些假设之上的数万行代码，然后以更可靠的计划重新开始；一个早期里程碑涉及 signalizer 函子定理，其候选证明依赖于仍需论证的结构性假设。随着智能体产生证明的速度快于 Lean 重新检查的速度，构建时间也成为瓶颈。Axiom 表示，其工程师将缓存的构建结果分发到各工作节点，并行运行独立检查，并将昂贵的有限计算外化为可单独检查的证书，该公司称这些更改将验证速度提高了几个数量级。

该公司叙述道，2026 年 10 月 10 日，频道中的一条消息宣布智能体已证明 Monster 是单群；智能体还通过 Griess 代数形式化了 Monster 的存在性，并证明了一个将 Monster 型群等同于 Monster 的定理。2026 年 10 月 13 日，只有一个里程碑关闭，工程师组织了一次重新规划工作，将未完成的里程碑拆分为更小、陈述精确的定理，每个分解都必须展示各部分如何通过简短的 Lean 证明来确立原始里程碑。

在已发表证明中发现缺口

Axiom 报告称，将证明翻译成 Lean 暴露了已发表论证中的问题。大多数是次要的——排版错误、表格错误或遗漏的假设——但该公司统计出 34 处与已发表记录值得注意的偏差，其中最实质的涉及非平衡群定理（UGT）。

一个例子来自 Aschbacher 和 Smith 的 quasithin 卷，其中一条引理断言两个数值量相等。智能体们发现了一个涉及群 SL₂(5) 的反例，其中一个量为 1，而所断言的等式要求为 2。将该等式替换为不等式修正了这条引理，但后续论证曾使用等式来排除某些情形，因此团队扩展了先前的论证以覆盖这些构型。

UGT 有助于从关于子群的信息中识别整个群：根据配套论文的摘要，在分类的归纳假设下，一个在 involutions 的中心化子中正规的非平凡奇阶子群会迫使环境单群为奇特征李型，或为特定次数的交错群。Axiom 通过 John Walter 1986 年的回忆录来研究 UGT，在形式化该论证时，其智能体们发现了它所使用的一个闭包断言的反例：一个被假定能使相关单群保持在指定族内的操作，可能产生一个被明确排除在该族之外的群。

在该公司的叙述中，从 PSL₂(49) 出发——其域对合的中心化子为 PGL₂(7)——该操作产生单分量 PSL₂(7)，而由于 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 的情况下得出了相同结论。

该论文《非平衡群定理》由 Colin Defant 和 Ken Ono 贡献，于 2026 年 10 月 27 日以 CC BY 4.0 许可作为第 1 版发布在 Hexagon 预印本服务器上；项目页面列出其篇幅为 35 页。Axiom 表示，它正与群论学家合作汇编文献中发现的勘误，并将发布在项目的勘误页面上。Lyons 和 Solomon 的工作为分类奠定了基础，他们就 UGT 的修补工作接受了咨询，该公司表示将继续与包括他们在内的顾问委员会以及外部顾问 Dan Nakano 一起整理和解决勘误。Axiom 将其贡献定位为使证明可机械检验、记录所遇到的障碍，并提供解决这些障碍的形式化论证，同时声明分类仍然是发现这些群并发展出这些论证的数学家的成就。