Axiom 用 AI 智能体群 24 天把「有限单群分类」形式化进 Lean：约 4310 万行代码，查出已发表证明中 34 处值得注意的偏差

「巨型定理」被机器核完

有限单群分类定理（CFSG）说的是：每个有限单群要么是素数阶循环群，要么是交错群，要么属于 16 个李型群无穷族，要么是 26 个散在单群之一。它常被称为史上最长的数学证明：原始证明约 1.5 万页、分布在 500 多篇文章里，由约 100 位数学家历经数十年完成，1983 年宣布完成后又因拟薄群的缺口拖到 2004 年才补上。

数学 AI 公司 Axiom Math 10 月 27 日宣布，已用 Lean 证明助手完成 CFSG 的完整形式化，每一步逻辑都经 Lean 内核检查。按官方说法，工程师和数学家指挥由数十个 AI 智能体组成的「群」，从 10 月 1 日开 Slack 协作频道、10 月 2 日首批智能体上线算起历时 24 天，产出约 4310 万行 Lean 代码。代码和交互式证明地图已在 GitHub（AxiomMath/CFSG）和项目网站公开。

怎么组织几十个智能体

团队先依托已有的 Lean 成果和从文献整理出的证明地图，把工程拆成 108 个里程碑和约 380 个小任务。智能体通过 GitHub issue 认领任务，遇到尚未形式化的前置数学就分派给其他智能体，结果汇入共享仓库。牵头的智能体负责拆解难题并审查待证命题，人类数学家处理数学上的障碍，工程师负责让系统持续运转。

过程并不顺。早期一些看似可控的里程碑背后藏着巨大前提，智能体直接「假设」了它们，团队删掉了数万行建立在这些假设上的代码重来。证明产出速度一度超过 Lean 重新检查的速度，工程师为此搭了跨机器的构建缓存，并把昂贵的有限计算外包成可单独验证的证书。10 月 13 日只关闭了一个里程碑，团队又专门组织了一轮重新规划，把未完成的里程碑拆成更小、表述精确的定理。由于第二代证明（Gorenstein、Lyons、Solomon 等人的多卷本）至今未出齐，Axiom 形式化的是第一代证明。

查出的问题

形式化要求把读者能自行补上的细节全部写明，于是暴露出已发表证明里的问题。大多数是笔误、表格错误、遗漏的假设，但有 34 处值得注意的偏差。一个例子来自 Aschbacher 与 Smith 关于拟薄群的著作：某引理断言两个数相等，智能体用群 SL₂(5) 找到反例，一个是 1、另一个需要是 2，改成不等式后，后续用到这一等式的论证要另行处理。

最重要的一处在「不平衡群定理」（UGT）。智能体在 John Walter 1986 年的论证中找到了一个闭包断言的反例，使关键推断失去依据，但并不推翻 UGT 的结论。团队与参与过 CFSG 的群论学家 Richard Lyons、Ronald Solomon 咨询后，基于 Solomon 1976 年的极大 2-分支理论走了另一条路，由 AxiomProver 证明并形式化了一个新的群论结果「简单顶的保持」。Axiom 表示会与群论学者一起整理勘误表并公开。

需要说明的是，以上勘误与修复目前都来自 Axiom 团队，尚待群论界独立复核；形式化核验的是 Lean 中的定理陈述与推导，陈述本身是否准确表达了 CFSG，仍需人来审。