形式化「巨大定理」（27分钟阅读）

# 形式化"巨大定理" 来源：https://axiommath.ai/research/the-enormous-theorem-formalized/ Axiom 已在 Lean 中形式化了有限单群分类定理——数学史上最長的证明。 今天，我们发布了有限单群分类定理（CFSG）的首个完整计算机验证证明。作为二十世纪数学的重大成就之一，该分类确定了有限群的基本构件。CFSG 被广泛认为是有史以来最长的人类数学证明，其原始证明跨越约 15,000 页，分布在约 100 位数学家撰写的 500 多篇论文中，因此获得了"巨大定理"的绰号。John Thompson 因在分类工作中做出的关键贡献，获得了菲尔兹奖（1970）和阿贝尔奖（2008）。在 24 天的时间里，Axiom Math 的工程师和数学家指挥了数十个 AI 智能体组成的群体，在该项目中产生了约 4310 万行 Lean 证明助手代码。 [群](https://en.wikipedia.org/wiki/Group_(mathematics))是描述对称性的基本对象，在本科数学的早期阶段就会介绍。以一个立方体为例：它有 24 种旋转方式使其外观与旋转前完全一致——其 6 个面中的任何一个都可以旋转到顶部，且有四种朝向。将其中两种旋转复合会得到 24 种之一，且每种旋转都有逆元。群就是具有这两个性质的变换的集合。一副纸牌的排列则提供了有限群的一个大得多的例子。 有限群可以在[Jordan–Hölder 定理](https://en.wikipedia.org/wiki/Composition_series#Uniqueness:_Jordan%E2%80%93H%C3%B6lder_theorem)所给出的意义下分解为不可分解的因子。这些因子——有限群的"原子"——就是[有限单群](https://en.wikipedia.org/wiki/Simple_group)。分类定理给出了这些构件的完整列表：有限对称性的元素周期表。 为了形式化该证明，我们将其重写为 [Lean](https://lean-lang.org/) 代码——一种数学定义、命题和证明可以写得足够精确以供计算机逐步检查的编程语言。将 CFSG 相关工作翻译到 Lean 的过程中暴露了已发表论证中的一些问题。大多数是小问题，如排版错误、表格错误或遗漏的假设条件。但有 34 处与已发表文献存在显著偏差需要解决，其中最重大的涉及非平衡群定理（Unbalanced Group Theorem）。这项工作还产生了一个群论新结果，其陈述和在证明中的作用在下文讨论。经与分类工作所依赖的数位群论专家磋商后，我们将发布详细的勘误清单，以供所有人参考。 CFSG 所分类的有限单群也出现在数学物理中，在那里对称性有助于组织量子系统可能的状态。例如，最大的有限单群——[魔群](https://en.wikipedia.org/wiki/Monster_group)——作为 Igor Frenkel、James Lepowsky 和 Arne Meurman 构造的一个量子理论的对称群出现。该理论为[月光猜想](https://en.wikipedia.org/wiki/Monstrous_moonshine)赋予了数学实质——一种魔群与模函数之间出乎意料的联系，其核心猜想由 Richard Borcherds 证明，该成就使他获得了 1998 年的菲尔兹奖。2007 年，物理学家兼菲尔兹奖得主 Edward Witten 提出，该理论可以描述一个具有二维空间和一维时间的简化宇宙中的引力。在该方案中，与魔群相关的数学将编码黑洞量子态在各能级间的分布，将最大的散在群与[黑洞熵](https://en.wikipedia.org/wiki/Black_hole_thermodynamics)问题联系起来。一项相关进展——[幽影月光猜想](https://en.wikipedia.org/wiki/Umbral_moonshine)——将其他有限群与称为 mock 模形式的函数联系起来，并促使人们进一步研究这些对称性与弦论之间的关系。 ## 对称性的周期表 有限单群居然可以如此分类，这本身就是令人惊讶的！某些数学结构足够刚性，以至于从一开始就似乎可以对其进行分类。例如，[有限域](https://en.wikipedia.org/wiki/Field_(mathematics)#Finite_fields)是一个有限数系，具备加法、减法、乘法以及对非零元素的除法。除了元素的重新标记之外，有限域由其大小完全确定，而可能的大小恰好是素数幂。其算术性质对其形态施加了强有力的约束。 群则享有大得多的多样性。即使将注意力限制在单群上，也几乎没有直接的理由期望所有可能性都能被简洁而紧凑地描述。发现许多例子并不能证明搜索总会结束；分类定理必须解释为什么每一个可想象的有限单群都被迫出现在列表中。CFSG 确立了该列表由素[阶](https://en.wikipedia.org/wiki/Order_(group_theory))的[循环群](https://en.wikipedia.org/wiki/Cyclic_group)、作用在至少五个符号上的[交错群](https://en.wikipedia.org/wiki/Alternating_group)、以及在有限域上构造的十六个无限[李型群](https://en.wikipedia.org/wiki/Group_of_Lie_type)族组成，此外恰好有 26 个孤立的[散在群](https://en.wikipedia.org/wiki/Sporadic_group)。CFSG 的大部分困难在于证明这些确实穷尽了所有可能性。 有限对称性的周期表：无限族（循环群、交错群和十六个李型群族）以及二十六个散在群。 来源：S. D. Smith；有限群表示图册（ATLAS of Finite Group Representations）。 Émile Mathieu 在 1860 年代和 1870 年代发现了最初的五个散在群。近一个世纪之后，Zvonimir Janko 于 1965 年发现了另一个。随后又有更多发现，最终导致了最大散在群——魔群的发现，其元素个数约为 $8 \times 10^{53}$。 Bernd Fischer 和 Robert Griess 于 1973 年独立预言了魔群的存在。1980 年，Griess 使用一个维度为 196,884 的[代数](https://en.wikipedia.org/wiki/Griess_algebra)构造了它。魔群的存在本身就是一个重大的数学成就。分类定理进一步断言，对有限单群的搜索是穷尽的：每个有限单群都属于某个无限族，或者是 26 个散在群之一。 ## 组装巨大定理 对有限单群候选列表的搜索与另一项工作并行推进：证明该列表是完整的。在 1954 年国际数学家大会的演讲中，Richard Brauer 强调了一种通过研究与二阶元素交换的对称性来识别单群的策略。这样的元素称为[对合](https://en.wikipedia.org/wiki/Involution_(mathematics)#Group_theory)。与其交换的对称群——称为其[中心化子](https://en.wikipedia.org/wiki/Centralizer_and_normalizer)——成为分类计划的核心对象。 1963 年，Walter Feit 和 John Thompson[证明](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem)了每个非阿贝尔有限单群都具有偶数阶。由此（[Cauchy 定理](https://en.wikipedia.org/wiki/Cauchy%27s_theorem_(group_theory))），每个这样的群都包含一个对合，使得对合中心化子的研究在整个分类中都适用。他们的证明长达 255 页，占满了《太平洋数学杂志》[一整期](https://projecteuclid.org/journals/pacific-journal-of-mathematics/volume-13/issue-3)。2012 年，Georges Gonthier 领导的团队经过六年协作努力，在 Coq（现名 Rocq）中完成了 Feit–Thompson 定理的里程碑式形式化。这是首次证明如此深度和复杂性的数学证明可以被计算机完全验证的示范之一。 1972 年，Daniel Gorenstein 提出了完成分类的十六步计划。在接下来的十年里，一个庞大的群论家社群发展了执行该计划所需的定理。这些结果逐步筛选有限单群的候选者，最终得到一个可以与 CFSG 陈述中的列表相对应的集合。1983 年，Gorenstein 宣布分类已经完成，后来称之为"巨大定理"。 有限单群分类从 1832 年 Galois 到 2026 年 Axiom 形式化的时间线。 1950 年之前的时间轴已压缩。 ## 两代证明：完成与重组 1983 年的宣布被证明为时过早。一个重要案例涉及[拟薄群](https://en.wikipedia.org/wiki/Quasithin_group)，依赖于 Geoffrey Mason 一份未完成的手稿。这个缺口直到 Michael Aschbacher 和 Stephen Smith 于 2004 年发表了一篇 1,221 页的处理才得以填补。这结束了现在被称为"第一代证明"的工作。随后又有修正工作，包括 Koichiro Harada 和 Ronald Solomon 在 2008 年的工作，填补了涉及散在 Mathieu 群 M22 的另一个缺口。 文献的规模和分散性使得整体检查第一代证明异常困难。各项结果依赖于散布在数十年间论文中的其他结果，有时使用不同的记号或以不同方式组织数学内容。理解这些论证如何衔接需要相当深厚的专业知识。 从 1980 年代末开始，Gorenstein 和 Lyons——后来 Solomon 和 Inna Capdeboscq 加入——发展了更系统的[第二代证明](https://en.wikipedia.org/wiki/Classification_of_finite_simple_groups#Second-generation_classification)。他们多卷本的处理重组了数学内容，简化了论证，使整体结构更易理解。Gorenstein 于 1992 年去世，但项目继续推进。到 2023 年，已有十卷出版；在撰写本文时，预计至少将有十二卷。 这项工作反映了建立和保存如此规模定理所需的持续努力。Aschbacher 在 2005 年写道："要写出一个非常长且复杂的论证而不出错是不可能的。"分类的历史包含了数十年的审查、修正和替代证明。 形式化在这些工作的基础上，显式地记录假设和推导，并检查它们如何衔接在一起。当必要的论证缺失时，形式化不会继续推进，直到缺口被填补：该步骤必须得到论证，其陈述必须被修正，或者必须提供另一条路径。因此，将 CFSG 的数学转化为完整的 Lean 证明意味着填补整个文献体系中的每一个此类缺口。Axiom 通过协调大量同时进行的形式化工作，并将每个结果与最终的分类陈述保持关联来实现这一目标。 ## 释放智能体群 形式化 CFSG 意味着将庞大的数学论证网络转化为一个所有依赖关系都可以被检查的单一证明。一个智能体可能成功形式化了一个困难的定理，但该定理只有在其定义和假设与证明其余部分的要求一致时才能对分类做出贡献。在这个规模上协调数学工作是一项全新的重大任务。 应该形式化第一代证明还是第二代证明？第二代证明仍然不完整。因此，目标不仅是形式化 CFSG 的*某个*证明，而是形式化*第一代证明*，这隐含地限制了可以使用的数学方法。 2026 年 10 月 1 日，我们开设了一个 Slack 频道来协调该项目。基础建立在 [Lean 中已有的工作](https://github.com/AxiomMath/CFSG/blob/main/CFSG/ThirdParty/README.md)以及从已发表文献中整理的内部证明图之上。两者共同将项目划分为 108 个里程碑和约 380 个更小的任务。 证明图为智能体提供了一个关于需要证明什么以及各部分之间如何相互依赖的共同说明。一个智能体可以认领一个任务，找到相关的论证，然后开始将其翻译为 Lean 代码。当某个任务需要尚未形式化的数学时，它可以将这些前置工作委派给其他智能体。结果被输入到一个共享仓库中，其他工作者可以使用这些结果。 AxiomProver 的智能体分工协作。主控智能体分解困难的论证并审查正在形式化的命题。其他智能体搜索已有结果或专注于编写 Lean 证明。智能体使用不断变化的模型组合，协调工具辅助其工作。人类数学家研究数学障碍，而工程师则维持不断增长的系统高效运行。 10 月 2 日，第一批智能体群上线。智能体通过 GitHub issues 认领里程碑，并在 Slack 中报告完成的工作。 早期进展暴露了初始计划的弱点。一些看起来可控的里程碑隐藏了巨大的前置条件，而这些前置条件被智能体假设了而非证明了。我们删除了基于这些假设构建的数万行代码，并以更可靠的部分计划重新开始部分工作。一个早期里程碑涉及[信号化函子](https://en.wikipedia.org/wiki/Signalizer_functor)定理，该定理解释了相容的局部子群如何组合在一起。一个候选证明依赖于仍需证明的额外结构性假设。条件证明仍有用，但完成该里程碑需要证明缺失的那部分联系。 一个反复出现的困难是判断在定理中添加假设是推迟了工作还是改变了其含义。完成一个里程碑意味着证明了分类所需的某个定理。一个候选证明可能在附加的未证明假设下建立了所需的结论，从而留下原始里程碑未完成。因此，审查工作必须将已证明的命题与预期目标进行比较，并判断任何附加假设是否可以从定理的已述假设中推出。 ## 保持证明的连贯性 保持证明的连贯性需要不断对其进行检查。随着仓库的增长，构建时间成为了瓶颈：智能体产生证明的速度超过了 Lean 重新检查的速度，而更改一个共享结果可能迫使 Lean 重新检查所有依赖它的结果。当智能体在不同机器上工作时，这项工作也可能在群中被重复执行。我们的工程师开发了一个系统，将缓存的构建结果分发给各个工作者并行运行独立检查，在代码及其依赖未更改时重用之前的结果。此外，昂贵的有限计算被外部化为可以单独检查的证书。这使验证速度提高了数个数量级。 每个新结果都必须融入一个被许多智能体同时修改的库中。对单个定义的多种表述必须保持兼容，昂贵的计算需要在不重复劳动的情况下被检查，而智能体需要复用已有的数学内容，而非重新实现后再进行协调。其他智能体专注于集成工作：从最终的分类定理回溯其前提条件，找出错误……