Axiom Math 发布 43.1M-Line Lean 分类证明

AI 模型和平台

Axiom Math 发布 43.1M-Line Lean 分类证明

在 Google 上的首选来源中添加 Unite.AI

2026年10月27日Axiom Math 称发布它所谓的"Finite Simple Groups分类"的首个完整的计算机检查证明，由工程师和数学家在24天内制作出，指导数十个AI agents在Lean证明助手中写了大约4,310万行代码。

该公司在公告中写道，“今天，我们正在公布《有限简易团体分类》的第一个完整的计算机核对证明”。 分类确定了有限群的基本构件，其原始证据在大约100位数学家的500多篇文章中延伸了约15,000页，这个尺度为它赢得了巨大的定理的绰号。

何为轴发布

CFSG规定，每个有限的简单组群都是主序的循环，交替在至少五个符号上，一个是在有限球场上构建的Lie类型的组群的16个无限家族之一，或者一个完全26个孤立的零星组群；指出宣布一些作者将Tits组群算作第27个。 最大的零星群"怪兽"是由罗伯特·格里斯(Robert Griess)于1980年用维数196,884的代数建造的。

人类的证明努力持续了几十年。 1963年，沃尔特·费特和约翰·汤普森(英语：John Thompson)证明每个非亚伯利亚人有限的简单群体甚至有秩序，在一份255页的论文中，填补了太平洋数学期刊的整期。 丹尼尔·戈伦斯坦(Daniel Gorenstein)在1972年制定了完成分类的十六步程序，并于1983年宣布完成，但准辛案依赖于杰弗里·梅森(Geoffrey Mason)的未完成手稿，直到迈克尔·阿施巴赫尔(Michael Aschbacher)和史蒂芬·史密斯(Stephen Smith)在2004年发表了一份长达1,221页的处理结果，结束了被称为第一代证明。 戈伦斯坦和理查德·里昂斯开始的更系统的第二代证据，后来罗纳德·所罗门和因纳·卡普德博斯克(英语：Inna Capdeboscq)也加入其中，仍然不完整，因此阿克森姆将第一代证据正式化。

计划页面将形式化为第一代证据，由Lean的内核检查每个逻辑步骤，Axiom 称的证明地图借鉴了第二代的卷，形式化中包含了来自早先的Qiuzhen-CFSG项目的大约120万行代码，并以Mathlib为基础，它信用于数百名贡献者。 项目命名为迪安·库雷顿，瓦西里·伊林，巴维克·梅赫塔，尼尔斯·沃斯为核心贡献者，列东宏为主要调查者。

公共的GitHub寄存器将结果描述为一种无忧无虑的Lean4证明，被钉在4.35.0-rc3版本上，建立在Mathlib和TauCeti项目上，并且只使用标准的轴心经典。 选择，propext，和 Quot. sound，没有本地决定。 它关于分类的正式说明取自TauCeti，其内容如下：“每个有限的简单组别都与分类清单上明确构成的组别之一不同。” README 称湖建设检查整个开发过程，湖建设工具的开放修改和团队计划向上游优化，使建设时间不到24小时；代码带有Apache-2.0许可证。

24天的集群任务

2026年10月1日，Axiom开通Slack频道协调项目。 先前存在的Lean作品和从已出版文献组装的内部证明地图将工作分为108个里程碑和约380个较小的任务；第一批集群于2026年10月2日上线，agents声称通过GitHub问题实现里程碑，并在Slack报告已完成的工作。 领导agents解析了困难的论据并审查了语句，而其他agents搜索了现有的结果或写了Lean的证明，agent可以将缺失的先决条件委托给其他其结果进入共享寄存器的agents.

早期进展暴露出弱点。 一些显然可以管理的里程碑掩盖了agents假设而非证明的巨大先决条件，团队删除了数以万计基于这些假设的线条，然后重新开始实施更合理的计划；一个早期里程碑涉及信号器分泌器定理，其候选人的证明依赖于结构假设，而这些假设仍然需要说明理由。 Build times也成为瓶颈，因为agents生产的证明比Lean能够重新检查的速度快。 Axiom 称的工程师在工人之间分配缓存的建筑结果，平行进行独立检查，并将昂贵的有限计算外部化为可单独核查的证书，按数量级更改了称公司的速率核查。

2026年10月10日，宣布频道的一条消息称agents证明了"怪物"的简单，公司重新计票；agents还通过格里斯代数和一个定理将"怪物"类型组与"怪物"正式确定。 2026年10月13日，只有一个里程碑关闭，工程师组织重新规划工作，将未完成的里程碑分为较小的，准确表述的定理，每个分解需要通过一个简短的利恩证明来显示棋子将如何建立原始里程碑。

在公布的证据中发现的漏洞

将证据翻译为Lean，暴露了公开发表的论点中的问题，Axiom报告。 多数是轻微的——印刷错误、表格错误或推卸假设，但公司与公布的记录有34个值得注意的偏差，其中与未平衡的集团定理或UGT关系最大。

一个例子来自Aschbacher和Smith的准辛卷，一个lemma断言两个数值相等。 agents发现一个涉及SL2(5)组的反例，其中1个数量为1个，声称的平等要求为2个数量。 以不平等取代平等纠正了lemma，但后来的论据利用平等排除了案件，因此团队拓宽了早先的论据以涵盖这些配置。

UGT帮助从有关其分组的信息中识别出一个完整的组群：根据所附论文的抽象，在分类的诱导假说下，一个进化器中心化器中一个非三角单序分组的正常现象迫使环境简单组群在奇特特征中属于Lie类型或具有某种程度的交替。 Axiom通过John Walter1986年的回忆录接近UGT，虽然将这一论点正式化，但agents发现它使用的关闭断言的明显反例：假定将相关简单群体留在特定家庭的行动可以产生一个被明确排除在外的群体。

在公司的账户中，从PSL2(49)开始，其演化场拥有中央集成器PGL2(7)，操作产生简单的组件PSL2(7)，因为7是梅森内质而被排除在家庭之外。 Axiom 指出反例没有反驳UGT本身，甚至也没有反驳Walter提案II.5.9(二)的结论。

修复工作借鉴了所罗门1976年关于最大二元构件的理论，Axiom 称为其Axiom Prover系统产生和正式化的备选论点提供了中心思想。 论文中所说的关键步骤是定理2.3(保留简单的超过)，被Axiom描述为AxiomProver所证明的群论的新结果；结合吉尔曼和所罗门的减少以及Foote和Harris的识别定理，它提供了分类所需的UGT的简单群形式。 形式化后，Axiom数学家在第一代方法中发现了一个较短的推理，记录为Remark 9.5，在没有定理2.3的情况下得出相同的结论。

由科林·德凡特(Colin Defant)和肯·奥诺(Ken Ono)贡献的论文"不平衡的集团定理"于2026年10月27日作为版本1以CC BY 4.0的许可出现在六角预印服务器上；项目页面将其列出为35页。 Axiom 称正与团体理论家合作，Lyons和Solomon的工作是分类的基础，他们咨询了UGT的修理，称公司将继续通过一个包括他们在内的咨询委员会，与外部顾问Dan Nakano一起管理和解决错误。 Axiom将其贡献设定为使证明可以机械地核查，记录遇到的阻碍，并提供解决这些阻碍的正式论证，同时表示分类仍然是发现这些团体并发展论证的数学家的成就。

本文由 AI图鉴自动抓取并翻译，版权归原作者所有；如需查看原文请点下方链接。

AI Models & Platforms

Axiom Math Releases 43.1M-Line Lean Proof of Group Classification

Add Unite.AI to your preferred sources on Google

Axiom Math said on October 27, 2026 that it is releasing what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups, produced over 24 days by engineers and mathematicians directing swarms of dozens of AI agents that wrote approximately 43.1 million lines of code in the Lean proof assistant.

“Today, we are releasing the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG),” the company wrote in its announcement. The classification identifies the basic building blocks of finite groups, and its original proof extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, a scale that earned it the nickname the enormous theorem.

What Axiom Released

CFSG establishes that every finite simple group is cyclic of prime order, alternating on at least five symbols, one of sixteen infinite families of groups of Lie type constructed over finite fields, or one of exactly 26 isolated sporadic groups; the announcement notes that some authors count the Tits group as a 27th. The largest sporadic group, the Monster, was constructed by Robert Griess in 1980 using an algebra of dimension 196,884.

The human proof effort stretched across decades. In 1963, Walter Feit and John Thompson proved that every nonabelian finite simple group has even order, in a 255-page paper that filled an entire issue of the Pacific Journal of Mathematics. Daniel Gorenstein laid out a sixteen-step program to finish the classification in 1972 and declared it complete in 1983, but the quasithin case rested on an unfinished manuscript by Geoffrey Mason until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004, closing what became known as the first-generation proof. A more systematic second-generation proof begun by Gorenstein and Richard Lyons, later joined by Ronald Solomon and Inna Capdeboscq, remains incomplete, so Axiom formalized the first-generation proof.

The project page presents the formalization as following the first-generation proof with every logical step checked by Lean’s kernel, and lists 43.1 million lines of Lean, 2.05 million declarations, and 715 papers and books in its corpus. Axiom says its proof map drew on the second-generation volumes, and that the formalization incorporates roughly 1.2 million lines of code from the earlier Qiuzhen-CFSG project and builds on Mathlib, which it credits to hundreds of contributors. The project names Dean Cureton, Vasily Ilin, Bhavik Mehta, and Niels Voss as core contributors, with Letong Hong as principal investigator.

The public GitHub repository describes the result as a sorry-free Lean4 proof, pinned to version 4.35.0-rc3, built on Mathlib and the TauCeti project and using only the standard axioms Classical.choice, propext, and Quot.sound, with no native_decide. Its formal statement of the classification, taken from TauCeti, reads: “Every finite simple group is isomorphic to one of the explicitly constructed groups on the classification list.” The README says lake build checks the entire development, and that open changes to the Lake build tool and optimizations the team plans to upstream brought build time under 24 hours; the code carries an Apache-2.0 license.

A 24-Day Swarm Effort

On October 1, 2026, Axiom opened a Slack channel to coordinate the project. Pre-existing Lean work and an internal proof map assembled from the published literature divided the effort into 108 milestones and about 380 smaller tasks; the first swarm went live on October 2, 2026, with agents claiming milestones through GitHub issues and reporting completed work in Slack. Lead agents decomposed difficult arguments and reviewed statements, while other agents searched for existing results or wrote Lean proofs, and an agent could delegate missing prerequisites to other agents whose results entered a shared repository.

Early progress exposed weak points. Some apparently manageable milestones concealed enormous prerequisites that agents had assumed rather than proved, and the team deleted tens of thousands of lines built on those assumptions before restarting on a sounder plan; one early milestone concerned the signalizer functor theorem, whose candidate proof relied on structural assumptions that still needed justification. Build times also became a bottleneck as agents produced proofs faster than Lean could recheck them. Axiom says its engineers distributed cached build results across workers, ran independent checks in parallel, and externalized expensive finite calculations into separately checkable certificates, changes the company says sped verification by orders of magnitude.

On October 10, 2026, a message in the channel announced that the agents had proved the Monster simple, the company recounts; the agents also formalized the Monster’s existence through the Griess algebra and a theorem identifying groups of Monster type with the Monster. On October 13, 2026, only one milestone closed, and engineers organized a replanning effort that split unfinished milestones into smaller, precisely stated theorems, each decomposition required to show how the pieces would establish the original milestone through a short Lean proof.

Gaps Found in the Published Proof

Translating the proof into Lean exposed problems in the published arguments, Axiom reports. Most were minor — typographical errors, errors in tables, or dropped hypotheses — but the company counts 34 noteworthy deviations from the published record, the most substantial relating to the Unbalanced Group Theorem, or UGT.

One example came from Aschbacher and Smith’s quasithin volumes, where a lemma asserted that two numerical quantities were equal. The agents found a counterexample involving the group SL₂(5), in which one quantity was 1 where the asserted equality required 2. Replacing the equality with an inequality corrected the lemma, but later arguments had used equality to rule out cases, so the team broadened an earlier argument to cover those configurations.

UGT helps identify a whole group from information about its subgroups: according to the abstract of the accompanying paper, under the classification’s inductive hypotheses, a nontrivial odd-order subgroup normal in the centralizer of an involution forces the ambient simple group to be of Lie type in odd characteristic or alternating of certain degrees. Axiom approached UGT through John Walter’s 1986 memoir, and while formalizing that argument its agents found explicit counterexamples to a closure assertion it used: an operation assumed to keep the associated simple groups within a specified family could produce a group explicitly excluded from it.

In the company’s account, starting from PSL₂(49), whose field involution has centralizer PGL₂(7), the operation yields the simple component PSL₂(7), which is excluded from the family because 7 is a Mersenne prime. Axiom notes the counterexamples did not refute UGT itself, or even the conclusion of Walter’s Proposition II.5.9(ii).

The repair drew on Solomon’s 1976 theory of maximal 2-components, which Axiom says supplied the central ideas for an alternative argument its AxiomProver system produced and formalized. The key step, stated in the paper as Theorem 2.3 (preservation of simple tops), is described by Axiom as a new result in group theory proved by AxiomProver; combined with the reductions of Gilman and Solomon and the recognition theorems of Foote and Harris, it supplies the simple-group form of UGT needed for the classification. After the formalization, Axiom mathematicians found a shorter deduction within first-generation methods, recorded as Remark 9.5, that reaches the same conclusion without Theorem 2.3.

That paper, The Unbalanced Group Theorem, contributed by Colin Defant and Ken Ono, appeared on the Hexagon preprint server as version 1 on October 27, 2026 under a CC BY 4.0 license; the project page lists it at 35 pages. Axiom says it is working with group theorists to compile the errata found in the literature and will publish them on the project’s errata page. Lyons and Solomon, whose work underpins the classification, were consulted on the UGT repair, and the company says it will keep curating and resolving the errata with an advisory board that includes them, alongside external advisor Dan Nakano. Axiom frames its contribution as making the proof mechanically checkable, documenting the obstructions encountered, and supplying formalized arguments that resolve them, while stating that the classification remains the achievement of the mathematicians who discovered the groups and developed the arguments.

Auto-fetched and translated by AI Atlas. All rights belong to the original author.