Axiom 用 AI 智能体 24 天完成有限单群分类定理的 Lean 完整形式化
Axiom 宣布完成有限单群分类定理的 Lean 自动形式化，该证明约 15000 页、涉及 500 多篇论文和约 100 位作者。约 4000 万行 Lean 代码由成群的 AI 智能体在 24 天内写出，数学家负责引导。Axiom 称今年初让 AxiomProver 写出正确的 10000 行 Lean 证明还需数周，此次进步归因于同时重建模型、harness 和基础设施三层。
材料给出 Axiom 用智能体集群形式化有限单群分类定理的规模与耗时，可与年初 AxiomProver 的效率作对照。
Rohan Paul· @rohanpaul_ai · X·2026-10-27 23:12· 1 小时前AI 评分74
AI 导读
Axiom 宣布完成有限单群分类定理的 Lean 自动形式化，这是数学史上最长的证明，原证明约 15000 页、500 多篇论文、约 100 位作者。约 4000 万行代码由成群的 AI 智能体在 24 天内写出，数学家负责引导。Axiom 称今年初 AxiomProver 写出正确的 10000 行 Lean 证明还需数周，此次进步归因于同时重建模型、harness 和基础设施三层。
正文 · 原文
可验证 AI 的重大胜利。
形式化数学证明正开始像软件一样规模化。
@axiommathai 重写了数学史上最长的证明，全部 15000 页，约 4000 万行 Lean。
成群的 AI 智能体在 24 天内写出，数学家负责引导。
Axiom 表示，今年年初，让 AxiomProver 写出一个正确的 10000 行 Lean 证明还需要数周的反复引导。而现在，这群智能体在 24 天内形式化了一个规模约为其 4000 倍的问题。
目标是有限单群分类：约 15000 页、500 多篇论文、约 100 位作者，且没有任何一位读者通读过全部内容。
Axiom 将这一跃升归功于同时重建三个层面：模型、harness 和基础设施。
人类历史上最大的数学证明现已通过计算机验证。 今天，Axiom 宣布完成有限单群分类——即“对称性周期表”——的完整 Lean 自动形式化。 约 15000 页，由跨越几代人的 100 多位数学家共同构建。在 X 查看被引用的帖子
来源：Rohan Paul · x.com
来源：RadarAI · aihot.news