Axiom 在 Lean 中形式化有限单群分类定理

2026年10月26日，作者：Axiom Axiom已在Lean中形式化了有限单群分类，这是数学史上最长的证明。 今天，我们发布首个完整的、经计算机检验的有限单群分类（CFSG）证明。作为二十世纪数学的主要成就之一，该分类确定了有限群的基本构建块。CFSG的原始证明被广泛认为是有史以来人类写下的最长数学证明，它横跨约100位数学家撰写的500多篇文章、总计约15,000页，为CFSG赢得了“巨大定理”的绰号。因其在分类工作中的关键贡献，John Thompson被授予菲尔兹奖（1970年）和阿贝尔奖（2008年）。在24天里，Axiom Math的工程师和数学家指挥数十个AI智能体组成的集群开展了一个项目，在Lean证明助手中生成了约4310万行代码。 群是描述对称性的基本对象，在本科数学早期就会引入。拿一个立方体来说。有24种旋转方式能让它看起来与之前完全相同：它的6个面中的任何一个都可以位于顶部，且有四种朝向。应用其中两种旋转会得到24种旋转中的另一种，并且任何旋转都有逆。群就是具有这两个性质的变换的集合。一副纸牌的排列提供了一个大得多的有限群例子。 有限群可以分解为不可分解的因子，其意义由Jordan–Hölder定理给出。这些因子是有限群的“原子”，即有限单群。该分类给出了这些构建块的完整列表：一张有限对称性的元素周期表。 为了形式化该证明，我们用Lean重写了它。Lean是一种编程语言，其中的数学定义、陈述和证明可以被精确地书写，足以让计算机检查每一步。将通向CFSG的工作翻译成Lean的过程暴露了已发表论证中的问题。大多数是次要问题，例如排版错误、表格错误或遗漏的假设。然而，有34处与已发表记录值得注意的偏差需要解决，其中最重要的与不平衡群定理有关。这项工作还在群论中产生了一个新结果，其陈述及在证明中的作用将在下文讨论。在与多位其工作构成该分类基础的专家群论学家协商后，我们将公布这份冗长的勘误表，以惠及所有人。 CFSG所分类的有限单群也出现在数学物理中，在那里对称性有助于组织量子系统的可能状态。例如，最大的有限单群——魔群（Monster group），充当了Igor Frenkel、James Lepowsky和Arne Meurman构建的一个量子理论的对称群。该理论为魔群月光（monstrous moonshine）提供了数学实质，这是魔群与模函数之间一个意想不到的联系，其核心猜想由Richard Borcherds证明，这一成就获得了1998年菲尔兹奖的认可。2007年，物理学家、菲尔兹奖得主Edward Witten提出，该理论可以描述一个具有两维空间和一维时间的简化宇宙中的引力。在该提议中，与魔群相关的数学将编码黑洞量子态在各能级上的分布，从而将最大的散在群与关于黑洞熵的问题联系起来。一个相关的发展——暗影月光（umbral moonshine）——将其他有限群与称为仿模形式的函数联系起来，并促使人们进一步研究这些对称性与弦理论之间的关系。 对称性的元素周期表 有限单群竟能接受这样的分类，这本身就令人惊讶！有些数学结构足够刚性，以至于分类从一开始就显得可信。例如，有限域是一个带有加法、减法、乘法以及除以非零元素的有限数系。除了重新标记其元素之外，有限域由其大小决定，而可能的大小恰好是素数幂。它们的算术对它们能是什么施加了很强的约束。 群则具有大得多的多样性。即使将注意力限制在单群上，也没有多少直接理由期望所有可能性都能被干净而紧凑地描述。发现许多例子并不能证明搜索终将结束；分类必须解释为什么每一个可想象的有限单群都被迫进入该列表。CFSG确立了该列表由素数阶循环群、至少五个符号上的交错群、在有限域上构造的十六个李型群无限族，以及恰好26个孤立的散在群组成。¹ CFSG的许多困难在于证明这些已穷尽所有可能性。 有限对称性的元素周期表：无限族（循环群、交错群和十六个李型族）以及二十六个散在群。 来源：S. D. Smith；有限群表示ATLAS。 Émile Mathieu在19世纪60年代和70年代发现了最初的五个散在群。近一个世纪后，Zvonimir Janko于1965年发现了另一个。更多发现接踵而至，最终发现了最大的散在群——魔群，其元素数量约为$8 \times 10^{53}$个。 Bernd Fischer和Robert Griess于1973年独立预测了魔群的存在。1980年，Griess使用一个196,884维的代数构造了它。魔群的存在本身就是一项重大数学成就。该分类进一步断言，对有限单群的搜索是穷尽的：每个有限单群都属于某个无限族，或者是26个散在群之一。 组装巨大定理 寻找有限单群候选列表的工作与另一项努力并行推进：证明该列表是完备的。在1954年向国际数学家大会所作的报告中，Richard Brauer强调了一种策略：通过研究与二阶元素交换的对称性来识别单群。这类元素称为对合。与对合交换的对称群，称为其对合中心化子，成为分类纲领中的核心对象。 1963年，Walter Feit和John Thompson证明了每个非阿贝尔有限单群都具有偶数阶。因此，每个这样的群都包含一个对合，使得对合中心化子的研究适用于整个分类过程。他们的证明长达255页，占满了《太平洋数学杂志》的整整一期。 1972年，Daniel Gorenstein提出了一个十六步计划以完成分类。在接下来的十年里，一大批群论学家发展了实施该计划所需的各种定理。这些成果逐步筛选了有限单群的候选者，最终得到了一个可与CFSG陈述中列表相对应的集合。1983年，Gorenstein宣布分类已经完成，后来称之为“ enormous theorem”。 从1832年Galois到2026年Axiom形式化的有限单群分类时间线。 坐标轴在1950年之前经过压缩。 两代证明：完成与重组 1983年的宣布被证明为时过早。一个涉及拟薄群的重要情形依赖于Geoffrey Mason一份未完成的手稿。这一缺口一直存在，直到Michael Aschbacher和Stephen Smith于2004年发表了长达1，221页的处理。这结束了现在所谓的“第一代证明”。随后出现了修正，包括Koichiro Harada和Ronald Solomon在2008年的工作，填补了另一个涉及零散Mathieu群M₂₂的缺口。 文献的规模和分散程度使得完整核查第一代证明异常困难。结果依赖于数十年来撰写的论文中散布的其他结果，有时使用不同的记号或以不同的方式组织数学内容。理解这些论证如何相互配合需要大量的专业知识。 从20世纪80年代末开始，Gorenstein和Lyons，后来Solomon以及再后来的Inna Capdeboscq加入，发展了更为系统的第二代证明。他们的多卷本处理重新组织了数学内容，简化了论证，并使整体结构更易于理解。Gorenstein于1992年去世，但项目继续进行。到2023年，已出版十卷；截至本文写作时，预计至少将有十二卷。 这项工作反映了建立和保存如此规模定理所需的持续努力。Aschbacher在2005年写道：“不可能写出一个非常漫长且复杂的论证而不出现错误。”分类的历史包括数十年的审查、修正和替代证明。 形式化建立在这些工作之上，通过明确记录假设和推导，并检查它们如何相互配合。当缺少必要的论证时，形式化不会继续推进，直到缺口被填补：该步骤必须被证明合理、其陈述被修正，或提供另一条路径。因此，将CFSG的数学内容转化为完整的Lean证明，意味着要在整个工作体系中填补每一个这样的缺口。Axiom通过协调许多同时进行的形式化工作，并保持每个结果与最终分类陈述相关联，做到了这一点。 释放集群 形式化CFSG意味着将庞大的数学论证网络转化为一个其依赖关系均可被检查的单一证明。一个智能体可能成功形式化了一个困难的定理，但只有当该定理的定义和假设与证明其余部分所需的一致时，它才会对分类有所贡献。在这种规模上协调数学内容是一项新的、艰巨的任务。 应该形式化第一代证明还是第二代证明？第二代证明仍然不完整。因此，目标不仅是形式化CFSG的某个证明，而是形式化第一代证明，这隐含地限制了所采用的数学方法。 2026年10月1日，我们开设了一个Slack频道来协调该项目。基础建立在Lean中已有的工作以及一个根据已发表文献汇编的内部证明地图之上。它们共同将项目划分为108个里程碑和约380个较小的任务。 证明地图为智能体提供了关于需要证明什么以及各部分如何相互依赖的共享说明。一个智能体可以认领一项任务，定位相关论证，并开始将其转化为Lean。当一项任务需要尚未形式化的数学内容时，它可以将这些前提委托给其他智能体。结果进入一个共享仓库，其他工作者可以在其中使用它们。 AxiomProver的智能体分工合作。主导智能体分解困难的论证并审查正在形式化的陈述。其他智能体搜索已有结果或专注于编写Lean证明。智能体使用了不断变化的模型组合，协调工具支持它们的工作。人类数学家研究数学障碍，而工程师则保持不断增长的系统高效运转。 10月2日，第一个集群上线。智能体通过GitHub议题认领里程碑，并在Slack中报告已完成的工作。 早期进展暴露了初始计划的弱点。一些看似可管理的里程碑隐藏着巨大的前提，智能体曾假设这些前提而非证明它们。我们删除了建立在那些假设之上的数万行代码，并在更可靠的计划上重新开始了部分工作。一个早期里程碑涉及信号函子定理，该定理解释了相容局部子群如何相互配合。一个候选证明依赖于仍需证明合理性的额外结构假设。该条件性证明仍然有用，但完成该里程碑需要证明那个缺失的关联。 一个反复出现的困难是判断向定理添加假设是推迟了工作还是改变了其含义。完成一个里程碑意味着证明分类所需的一个定理。一个候选证明可能在额外的、未经证明的假设下建立所需结论，从而使原里程碑仍未完成。因此，审查必须将被证明的陈述与预期目标进行比较，并判断任何额外假设是否可从定理所述前提中推出。 保持证明的连贯性 保持证明的连贯性需要不断检查它。随着仓库的增长，构建时间成为瓶颈：智能体生成证明的速度快于Lean重新检查它们的速度，而更改共享结果可能迫使Lean重新检查其所有依赖项。由于智能体在不同机器上工作，这项工作也可能在整个集群中重复。我们的工程师开发了一个系统，在工作者之间分发缓存的构建结果并并行运行独立检查，当代码及其依赖项未更改时重用先前的结果。此外，昂贵的有限计算被外化为可单独检查的证书。这将验证速度提高了几个数量级。 每个新结果都必须融入一个同时被许多智能体更改的库中。单个定义的多种表达必须保持兼容，昂贵的计算需要在避免重复努力的情况下进行检查，智能体需要重用现有数学，而不是先重现它然后再进行协调。其他智能体专注于集成：追溯最终分类定理通过其先决条件，找到缺失的连接，并使现有结果沿该链条可用。 10月10日，频道中出现了一条消息：“我们证明了Monster是单群。”智能体还通过Griess代数形式化了Monster的存在性，以及一个将“Monster型”群与Monster等同的定理。这些是不同的成就。构造一个群、证明它是单群，以及从结构信息中识别它，各自需要自己的论证。 进展仍然不均衡。10月13日，只有一个里程碑关闭，而且目标仍然过于粗略，无法清晰了解剩余的数学内容。我们的工程师组织了一次专门的重新规划工作，指派智能体将未完成的里程碑分解为更小、精确陈述的定理。每个提议的分解都必须解释这些更小的定理连同现有结果如何通过一个简短的Lean证明来建立原始里程碑。这使得更容易看出哪些更小的定理仍需证明，将工作分配给智能体，并追踪每个结果如何对分类做出贡献。 2026年10月2日至25日，108个里程碑中已完成的数量。 机器发现了什么 在Lean中检查CFSG证明的每个依赖项揭示了文献中的问题。人类读者可以凭经验提供缺失的论证，识别未陈述的假设，或根据预期论证解释作者的符号。形式化要求这些选择被明确表达。这可能意味着填写“常规”细节。有时，它揭示出所陈述的断言是错误的。 智能体在遇到可疑问题时将其记录下来。这些报告需要调查：形式化某一步骤的失败可能反映源中的错误、错误的解释，或智能体自身工作中的错误。大多数报告结果是无害的：拼写错误、表格错误、遗漏的假设，或从上下文中显而易见的步骤。少数需要真正的数学。由此产生的数据库是那次调查的记录，在可用时包含反例和建议的更正。我们将其作为勘误表提供给群论社区使用。² 一个例子来自Aschbacher和Smith的“quasithin”卷。一个引理断言两个数值量相等。智能体发现了一个涉及群SL₂(5)的反例：一个量是1，而所断言的相等要求为2。将相等替换为不等式纠正了该引理，但一些后来的论证曾使用相等来排除现在需要关注的情况。在证明的一个受影响部分中，团队扩展了先前的论证以处理这些情况，然后在那些配置不存在的地方应用了后来的论证。这种修订后的情况划分使证明能够在不依赖错误相等的情况下达到所需结论。 人类专业知识仍然至关重要。数学家调查了最重要的报告。包括Richard Lyons和Ronald Solomon在内的进行CFSG原始工作的群论学家，就论证及其在分类中的位置进行了咨询。在如此广泛的文献中，了解替代证明路线（或为什么看似自然的修复会导致循环论证）可能会改变项目的方向。最重要的例子涉及非平衡群定理（UGT），它受益于与Lyons和Solomon的通信。 重新路由UGT的证明 UGT有助于从关于其子群的信息中识别整个群。假设存在一个不在已知列表中的有限单群，并选择一个阶尽可能小的。在其真子群中出现的较小单群将已经被分类。在这个归纳假设下，当在与对合交换的对称性中出现特定的奇阶结构时，UGT识别整个群。这解决了剩余分类问题中的一个重要情况。 我们通过John Walter 1986年的回忆录来研究UGT。Walter的处理在CFSG的历史中占有重要地位：2013年，Michael Aschbacher将证明UGT和B-猜想归功于他，同时也承认了其他证明。更广泛的历史包括Gilman和Solomon将UGT归约为一系列所谓的识别问题，这些问题随后在一系列论文中得到处理。由于我们选择形式化第一代证明，我们检查了Walter的论证。 在形式化该论证的过程中，我们的智能体发现了沃尔特证明中所用闭包断言的反例。该论证假设某个特定操作会将相关的单群保持在指定族内，但该操作可能产生一个被明确排除在该族之外的群。这使得一个关键推论缺乏依据，但这些反例并未反驳UGT的预期目标，甚至也未反驳沃尔特命题II.5.9(ii)的结论。 因此，完成形式化需要为该步骤提供另一种依据，或采用不同的论证。转向另一种已发表的方法可能带来新的依赖关系，而每一种依赖关系都需要在我们使用之前给出形式证明。例如，UGT可以从实质性的第二代结果中推导出来，但纸面上简短的推导可能建立在大量额外形式化工作之上。我们需要一条通往UGT的可靠路径，其支撑数学能够与我们正在构建的第一代证明相连接。 对于对具体反例感兴趣的读者，请从PSL₂(49)开始，它属于沃尔特的族。其域对合——由49元域的二阶对称性诱导的自同构——的中心化子是PGL₂(7)，其单分量是PSL₂(7)。后一群被排除在该族之外，因为7是梅森素数。这里的对合是PSL₂(49)的自同构，而不是该单群的元素。 我们汇集了曾帮助发展CFSG的群论学家，包括理查德·莱昂斯和罗纳德·所罗门，就我们解决第一代证明缺陷的工作进行咨询，包括如何处理UGT的证明。莱昂斯帮助厘清了可用的证明路径，并将该障碍置于其历史背景中。所罗门1976年的极大2-分量理论为AxiomProver产生并形式化的替代论证提供了核心思想。 该论证追踪被比较的子群以及连接它们的对合。在CFSG证明这一阶段所需的特定假设下，它确立这些比较保持相关的单群。这一保持性结果是AxiomProver证明的群论新结果，在 accompanying paper 中表述为定理2.3（“单顶的保持性”）。结合吉尔曼和所罗门的归约以及富特和哈里斯的识别定理，该论证提供了分类所需的UGT的单群形式。 在形式化之后，Axiom的数学家在第一批方法中找到了一个实质性的捷径。这一更短的推导记录在论文的注9.5中，无需定理2.3即可达到所需的UGT结论。论文保留了较长的论证，因为它遵循AxiomProver形式化的路径，并确立了额外的保持性定理。论文呈现了两个论证及其假设，并明确说明了它们对早期数学的依赖。 从完成的片段到完成的证明 解决UGT提供了分类论证的一个必要部分。完成CFSG需要将该结果和其他中间结果与最终分类陈述连接起来。该开发工作必须确立所列群的存在性和单性，并对其参数施加适当的限制，并证明每个有限单群都出现在列表中。这些义务中的每一项都需要自己的论证，而沿途使用的每个数学前提都必须得到交代。 这使得在形式化过程中进展容易被夸大。Lean可以验证在额外假设下证明的结果，即使该假设尚未被确立。这样的结果可以帮助推进其他证明，同时留下实质性的数学任务未完成。一个正确证明的结果也可能与最终论证中所需的精确陈述不同，需要进一步工作将它们连接起来。统计已完成的结果有助于组织工作，但只有当各个片段形成一个没有遗留未证明假设的单一证明时，形式化才算完成。 最终检查还需要注意形式陈述实际说了什么。人类检查该陈述及其使用的定义，以确认它表达了预期的分类；Lean检查确立它的形式推导。这将人类审查集中在规范上，而将证明的检查留给机器。一个形式化开发是否重现特定历史论证的每一步是一个单独的问题，而UGT论证的替换说明了为什么形式化可能沿着不同的路径达到相同的数学结论。 完成的形式化在分类的证明中连接了这些结果。该发布标识了最终定理并记录了如何检查该开发，以便读者可以精确检查所确立的内容。该仓库还提供了支撑定义和结果，供进一步的数学工作使用。 为什么这很重要 整个代数、数论、组合学甚至数学物理学中的结果都使用有限单群的分类。一篇论文可能用几个词引用它，同时依赖于分布在数十年研究中的论证。形式化赋予了这种依赖关系一个明确、可检查的形式。数学家可以调查哪些结果支持特定步骤，检查精确的假设，并在后续工作中使用形式化的组件。 这些修复本身就是一项贡献。已发表论证中的缺口可能是局部可修复的，可能需要不同的证明路径，或者可能需要实质性的新论证。形式化通过要求提供缺失的推理来帮助区分这些情况。UGT事件提供了该过程的一个具体例子。 附带的UGT论文以其他群论学家可以研究和使用的形式解释了该修复背后的数学。它在它们所依赖的早期结果的背景下发展了替代论证和新的保持性定理。然后这些思想可以为进一步研究提供信息，形式化的论证可作为精确的、计算机检查的基础。 这一分类仍然是发现这些群并发展出识别它们的论证的数学家的成就，其源头可追溯到19世纪伽罗瓦和若尔当的开创性思想。我们的项目建立在这一工作、早期形式化以及Lean和Mathlib社区的基础之上。Axiom的贡献在于使证明可被机器检验，记录过程中遇到的障碍，并提供解决这些障碍的形式化论证。未来的工作可以在这些结果的基础上继续推进，其假设和依赖关系可供查验。 这并不是故事的终点；群论方面的工作仍在继续。我们将与由群论学家组成的顾问委员会合作，持续整理并解决勘误，委员会成员包括Richard Lyons和Ronald Solomon。我们感谢他们持续给予的慷慨支持与帮助。 了解更多 - 完整证明 - 依赖关系图 - 非平衡群定理的新证明 - 背景阅读：Ronald Solomon，“A brief history of the classification of the finite simple groups，” Bulletin of the AMS 38 (2001)，及其2018年后记；Daniel Gorenstein，“The Enormous Theorem，” Scientific American（1985年12月）。 脚注 ¹ 一些作者将Tits群计为第27个散在群。 致谢 我们的形式化只是一段漫长历史中的一小部分。这一分类是一百多位数学家的成果，包括Richard Brauer、Walter Feit、John Thompson、Daniel Gorenstein、Michael Aschbacher、Richard Lyons、Ronald Solomon、Stephen Smith、Robert Griess、Bernd Fischer、John Conway、George Glauberman、Koichiro Harada、John Walter以及许多其他人。虽然我们的形式化遵循第一代证明，但我们的证明图谱大量借鉴了Gorenstein、Lyons、Solomon和Inna Capdeboscq的第二代卷册。我们的Lean形式化证明建立在Mathlib之上，数百名贡献者使之成为可能，并纳入了来自Qiuzhen-CFSG的约120万行代码。我们感谢外部顾问Richard Lyons、Dan Nakano和Ron Solomon付出的时间与专业知识。 核心贡献者：Dean Cureton、Vasily Ilin、Bhavik Mehta、Niels Voss 其他贡献者：Rafael Cabral、Colin Defant、Erik Gregory、Aaron Hill、Letong Hong、Qinheping Hu、Dustin Jamner、Albert Jiang、Tadeusz Jordan、Andranik Kurghinyan、Kenny Lau、Jonathan Laurent、David Liang、Jannis Limperg、Simon Mahns、Brian Nugent、Connor Olson、Ken Ono、Eric Paul、Dhruv Rajan、Karun Ram、Charlie Ray、Ho Chung Siu、Ashvin A. Swaminathan、Jesse Thorner、Aleksey Tsaplin、Chenkai Wang