Axiom 用 AI 智能体集群完成有限单群分类定理形式化证明
原标题：Big win for verifiable AI.
92AI 研判分
Axiom 宣布利用 AI 智能体集群在 24 天内完成了数学史上最长证明——有限单群分类定理（CFSG）的 Lean 形式化，生成约 4000 万行代码。这一突破标志着可验证 AI 从实验室走向规模化应用，证明了多智能体协作在复杂逻辑推理任务中的巨大潜力。
报道正文
Rohan Paul (@rohanpaul_ai) · 2026-10-27 15
可验证 AI 的重大胜利。
形式化数学证明正开始像软件一样实现规模化。
@axiommathai 重写了数学史上篇幅最长的证明，共计 15,000 页，约 4,000 万行 Lean 代码。 由一群 AI Agent 在 24 天内完成编写，期间由数学家进行引导和把控。
Axiom 表示，今年年初时，要让 AxiomProver 写出一段正确的 10,000 行 Lean 证明，还需要花费数周时间反复调试。而如今，这群 Agent 仅用 24 天就形式化了规模约为前者 4,000 倍的问题。
目标对象是“有限单群分类定理”（Classification of Finite Simple Groups）：涉及约 15,000 页内容、500 多篇论文、近 100 位作者，且没有任何一位读者曾通读全部材料。
Axiom 将这一飞跃归功于同时重构了三个层面：模型、执行框架（harness）以及基础设施。
↳ 引用 @axiommathai (Axiom): 人类历史上最大的数学证明现已通过计算机验证。
今日，Axiom 宣布完成了对“有限单群分类定理”——即“对称性的元素周期表”——的完整 Lean 自动形式化。
该成果涵盖约 15,000 页内容，由跨代际的 100 多位数学家共同构建而成。
