Axiom 用 24 天完成有限单群分类定理的 Lean 形式化，4310 万行代码开源

杨梦 2026-10-29 09:05 北京

近一个月以来，AI 正逐步探入数学研究的腹地。10 月 6 日，OpenAI 在代码托管平台 GitHub 上一次性公开了 722 份由内部模型生成的数学手稿，涉及数百个开放问题；10 月 26 日，OpenAI 团队又公布了其模型在调和分析、计算复杂性理论和量子场论上的新发现。

AI 产出证明的速度越来越快，如何确认这些证明可信，就成了数学界必须面对的问题。

其中一种应对办法是形式化验证，即借助证明助手 Lean 等工具，把数学家用自然语言写成的证明逐句“翻译”成计算机能够检查的形式语言。论文中常见的“显然”“同理可得”在 Lean 里行不通，任何省略的推导和隐含的条件都必须写明，每一步推理都要经过 Lean 内核的逐条检查才算通过。

10 月 27 日，美国 AI 数学公司 Axiom 公开了一项体量罕见的成果，宣布其 AI 智能体已在 Lean 中为有限单群分类定理（CFSG）完成了完整的形式化。CFSG 的原始证明约 15,000 页，分散在 500 多篇论文中，出自约 100 位数学家之手，是人类数学史上篇幅最长的证明，人称“巨型定理”。

Axiom 的工程师和数学家调度数十个 AI 智能体，用 24 天写出约 4,310 万行 Lean 代码，目前已在 GitHub 将其开源。

图 | Axiom 绘制的有限单群分类定理证明蓝图，中心为分类定理本身，外圈按依赖层级排列各里程碑和定理。（来源：Axiom）

一份没人能读完的证明

数学家用“群”描述对称性。一个正方体有 24 种旋转方式能让它看上去和原来一模一样，这 24 种旋转连同它们的组合规则就构成一个群。整数可以分解为质数的乘积，有限群也可以层层拆解，最终得到无法再拆分的基本单元，即有限单群。

CFSG 给出了所有有限单群的完整名录：素数阶循环群、交替群、16 个由有限域构造的李型群家族，外加 26 个不属于任何家族的“散在群”。其中最大的魔群（Monster group）约有 8×10⁵³ 个元素。数学家常把这份名录比作对称性的元素周期表。

列出名录相对容易，难的是证明名录之外再无遗漏。这项工作从 20 世纪 50 年代起步，约翰·汤普森（John Thompson）因奠基性贡献获得 1970 年菲尔兹奖和 2008 年阿贝尔奖。1983 年，群论学家丹尼尔·戈伦斯坦（Daniel Gorenstein）宣布分类完成，但很快有人发现，其中“拟薄群”一类情形只依靠一份未完成的手稿。

这个缺口直到 2004 年才由迈克尔·阿施巴赫（Michael Aschbacher）和斯蒂芬·史密斯（Stephen Smith）用一部 1,221 页的专著补上，2008 年学界又修补了另一处漏洞。这些论文和专著共同构成了如今所说的“第一代证明”。

证明的分散也成了难题：不同年代的论文使用不同的记号和组织方式，结论之间层层引用，弄清它们如何拼接需要深厚的专门知识。

从 20 世纪 80 年代末开始，参与分类工作的学者着手撰写更系统的“第二代证明”，到 2023 年已出版 10 卷，预计至少需要 12 卷，至今仍未写完。与此同时，代数、数论、组合数学乃至数学物理中的大量结论都以 CFSG 为前提。

图 | 有限单群名录，包括循环群、交替群、16 个李型群家族和 26 个散在群。（来源：Axiom，据 S. D. 史密斯整理及《有限群表示图集》）

一家想“形式化验证一切”的公司

Axiom 成立于 2025 年 3 月，创始人兼 CEO 洪乐潼（Carina Hong）是在广州长大的 00 后。她高中时入选广东数学奥林匹克省队，在麻省理工学院（MIT）用三年修完数学与物理双学位，因本科期间的研究获得美国本科生数学研究最高奖项摩根奖（Morgan Prize），并以罗德学者身份赴牛津大学深造，在进入斯坦福大学读博期间辍学创业。

公司的“创始数学家”、数论学家小野健（Ken Ono）2025 年离开弗吉尼亚大学加入 Axiom，洪乐潼本科期间曾在他主持的暑期科研项目中做研究。公司先后完成 6,400 万美元种子轮和 2 亿美元 A 轮融资，估值已超 16 亿美元。

Axiom 把“形式化验证一切”当作使命，其智能体系统 AxiomProver 能调度多个 AI 智能体协同完成大型形式化任务。今年 8 月，团队完成了素数间隙领域“246 定理”的形式化，这一定理表明存在无穷多对相差不超过 246 的素数。

用小野健的话说：世界即将运行在没人读过的代码之上，证明的形式化是应对这一挑战的试验场。

CFSG 把这个试验场推到了极限。它体量最大、结构最分散，真正能读懂全部论证的人却越来越少。项目核心成员瓦西里·伊林（Vasily Ilin）在社交媒体上写道，真正理解这个证明的人大多已经退休或离世。在一份靠集体记忆维系的证明上做机器核验，对数学界是一项基础建设，也是对Axiom技术能力最直接的检验。

24 天里，推倒再重来

Axiom 并非从零起步。Lean 社区数百位贡献者共同维护的数学库 Mathlib 提供了大量基础定义和定理。在丘成桐的倡导下，清华大学求真书院学生联合丘成桐数学科学中心等机构推进的 CFSG 形式化项目此前已积累了大量群论代码，Axiom 将其中约 120 万行纳入了自己的工程。

团队参照第二代证明的多卷著作绘制了一张证明地图，把整套论证拆成 108 个里程碑、约 380 项子任务。但由于第二代证明尚未写完，形式化的对象定为第一代证明。

10 月 2 日，第一批智能体集群上线。负责统筹的智能体拆解复杂论证、审核待证命题的表述，其余智能体检索已有结论、编写 Lean 代码。某项任务依赖尚未完成的前置结论时，系统会把这部分交给其他智能体，完成的结果汇入共享代码库供后续调用。人类数学家处理数学上的卡点，工程师维持系统运转。

起初的推进并不顺利。早期一些看似可控的里程碑背后藏着大量尚未证明的前提，智能体直接把它们当成既定事实写了下去。团队删掉了建立在这些假设上的数万行代码，部分工作因此必须推倒重来。

10 月 10 日，项目频道里传来消息，魔群的单群性证明完成。智能体还同时证明了魔群的存在，这是整个分类中最关键的环节之一。

公司记录显示，3 天后，进度突然陷入停滞，当天只完成了 1 个里程碑。工程师很快意识到，问题出在里程碑划分过粗，剩余工作量难以判断，于是他们重新规划，把未完成的里程碑拆成更小、表述更精确的定理。

代码规模膨胀也带来了新的问题。智能体写证明的速度超过了 Lean 重新检查的速度，改动一处共享结论，所有依赖它的内容都要重新校验，分布在不同机器上的智能体还会重复计算。工程师为此搭建了缓存分发系统，未改动的代码直接复用此前的检查结果，整体校验速度提升了几个数量级。

10 月 26 日，形式化完成。Lean 内核确认，从基础公理出发直到最终的分类定理，所有推理环节首尾相接。形式化陈述是否准确表达了数学家心目中的 CFSG，仍需要人类审阅，Axiom 在发布时邀请群论学者和 Lean 社区重新运行检查，并核对定理陈述与原定理是否一致。

图 | 10 月 2 日至 25 日，108 个里程碑的完成情况（来源：Axiom）

逐行核对的过程，也是对文献的一次彻底体检。智能体在形式化中记录下大量疑点，其中不少源于智能体自身的误读，需要人工逐一排查。已得到确认的问题大多是笔误、表格数据错误和遗漏的前提条件，另有 34 处与已发表文献的偏差需要专门处理。Axiom 表示将与群论学者合作，把整理好的勘误表公开给学界。

最棘手的问题出现在非平衡群定理（Unbalanced Group Theorem）。分类证明的基本思路是反证：假设存在一个不在名录上的单群，取其中最小的一个，再逐一排除它可能具有的结构。非平衡群定理负责排除其中一大类情形，是通往最终结论的必经环节。

团队沿用群论学家约翰·沃尔特（John Walter）1986 年的论证，智能体却在其中一条断言上找到了明确的反例。原文认为某种操作产生的单群始终留在一个特定的群族之内，实际上它可以产生恰好被排除在该族之外的群。反例没有推翻定理本身，但原论证的关键一步失去了依据。

换一条已发表的证明路线并不轻松，每条新路线都会牵出一批尚未形式化的前置结果，工作量可能成倍增长。

团队为此请教了当年参与分类工作的理查德·莱昂斯（Richard Lyons）和罗纳德·所罗门（Ronald Solomon）。理查德帮助梳理了可行的证明路线及其历史脉络，罗纳德 1976 年提出的“极大 2-分量”理论则提供了替代论证的核心思路。

AxiomProver 据此构造并形式化了一条新的论证路线，其间证明了一个此前没有的群论结果，相关论文已发布在预印本平台 Hexagon。

形式化完成后，Axiom 的数学家又在第一代证明的方法框架内找到一条更短的推导，不借助这一新定理也能得到所需结论，论文因此同时保留了两条路线。

谁来理解机器写下的证明？

就在 Axiom 发布成果的前一周，陶哲轩与邓煜在非营利机构 SAIR 基金会（SAIR Foundation）的播客中讨论了 AI 与数学的关系。OpenAI 的批量发布此前已在数学界引发激烈争论，9 月，两人与其他 23 位菲尔兹奖得主联名发表声明，批评 AI 公司把攻克数学难题当作模型能力的基准测试。

邓煜在对谈中区分了两条边界：一条圈定已经有证明的问题，另一条圈定人类能够理解其证明的问题。过去，两条边界几乎重合，有证明就有人懂；但如今出现了只有 AI 才懂的证明，两条边界开始分离。

他认为，AI 能把事情做好的前提，是人类已经充分理解问题、手里有证明的整体思路。陶哲轩则把 AI 公司批量解题的产出形容为模型训练中的某种“有毒废料”，最终要由数学家来消化处理。他希望 AI 公司在项目启动之初就请数学家加入，避免事后由学界收拾残局。

CFSG 项目和两人描述的理想状态有不少重合之处。它处理的是一份已有路线图的证明，第一代证明和第二代证明的多卷著作为智能体指明了方向；原始证明的参与者在关键节点介入，并将继续以顾问身份参与勘误整理。形式化过程也从方法层面回应了数学界对 AI 证明难以核验的担忧。

今年 6 月，得到国际数学联盟（IMU）支持的《AI 与数学莱顿宣言》将结果不可靠列为 AI 带来的风险之首，并强调人类应当为数学结论的正确性负责。

CFSG 被多个数学细分领域引用了几十年，但它却一直分散在数百篇论文中，没人能完整核验所有结论。如今，所有前提条件、推导依赖都变成了可追溯的代码，任何研究者可以顺着依赖链查到每一步论证的源头，也可以直接复用已完成的数学模块开展后续研究。正如 Axiom 在公告中所写：这不是故事的终点，群论领域的工作仍在继续。

数学的可靠性长久以来建立在同行之间的信任上，人们相信审稿人读懂了论证，相信前人没有出错。

但当越来越多的证明出自机器之手，这份信任需要新的支点，比如一份任何人都能重新运行、逐步核对的形式化证明。如果 AI 能接手繁琐的验证过程，数学家就能留出更多心力解决机器尚不擅长的事：提出值得追问的问题，同时在证明之外寻求理解。

参考内容：

https://axiommath.ai/research/the-enormous-theorem-formalized/

https://github.com/AxiomMath/CFSG

https://hexagonmath.org/2610.00575?version=1

https://spectrum.ieee.org/axiom-math-246-theorem-formalization

https://www.thepaper.cn/newsDetail_forward_34296807

https://leidendeclaration.ai/

注：首图/封面由 AI 辅助制作

跳转微信打开