Axiom 用 Agent 群 24 天在 Lean 中形式化有限单群分类定理

Axiom 10 月 26 日宣布完成有限单群分类定理（CFSG）第一代证明的 Lean 形式化，约 43.1 million 行代码、2.05 million 条声明，由 Lean 内核检查每一步推理。项目历时 24 天，几十个 AI Agent 分工拆解论证、检索已有结果和编写证明，人类数学家与工程师负责指挥、处理数学障碍并搭建构建缓存与并行检查系统。

要点

• Agent 发现 1986 年无平衡群定理证明中的一个封闭性断言不成立，团队另写了替代论证
• 项目处理了 34 处与已发表文献的明显偏差，计划公布勘误清单
• 人类仍需审查形式化的定理陈述和定义是否表达了原本的分类结论
• 项目拆成 108 个里程碑、约 380 个任务，未公布算力或成本

来源

### [Axiom 用 Agent 群 24 天在 Lean 中形式化有限单群分类定理]({{URL}})

Axiom 10 月 26 日宣布完成有限单群分类定理（CFSG）第一代证明的 Lean 形式化，约 43.1 million 行代码、2.05 million 条声明，由 Lean 内核检查每一步推理。项目历时 24 天，几十个 AI Agent 分工拆解论证、检索已有结果和编写证明，人类数学家与工程师负责指挥、处理数学障碍并搭建构建缓存与并行检查系统。

- Agent 发现 1986 年无平衡群定理证明中的一个封闭性断言不成立，团队另写了替代论证
- 项目处理了 34 处与已发表文献的明显偏差，计划公布勘误清单
- 人类仍需审查形式化的定理陈述和定义是否表达了原本的分类结论
- 项目拆成 108 个里程碑、约 380 个任务，未公布算力或成本

**为什么值得关注**：说明「Agent 群 + 机器可检查的验证器」能撑起超大规模任务，人主要负责拆解、把关陈述和处理疑难；对读者是方法上的参照，了解即可。

来源：[The enormous theorem, formalized](https://axiommath.ai/research/the-enormous-theorem-formalized/)；[CFSG in Lean](https://cfsg.axiommath.ai/)；[Hacker News 讨论：Classification of Finite Simple Groups Formalized in Lean](https://news.ycombinator.com/item?id=50261647)