数学史上最长证明获完整计算机验证：Axiom Math用AI形式化有限单群分类定理
talkingdev • 2026-10-28
1901 views
近日，Axiom Math发布了有限单群分类定理（CFSG）的首个完整计算机检查证明，这是数学史上的一项重大里程碑。CFSG被公认为人类写过的最长数学证明，原始证明横跨约15000页、500多篇论文，由约100位数学家共同完成。Axiom Math的工程师与数学家利用数十个AI智能体集群，在24天内于Lean证明助手中生成约4310万行代码，完成了这一庞大定理的形式化验证。该成果不仅意味着这一被称为“庞大定理”的数学基石获得机器可检验的可靠性保障，也展示了AI智能体协同与形式化证明工具结合的巨大潜力，可能深刻改变未来数学研究与验证的方式。
核心要点
- Axiom Math发布有限单群分类定理（CFSG）的首个完整计算机可检查证明
- 原始证明约15000页、500余篇论文、由近百位数学家完成，是史上最长数学证明
- 项目在24天内利用数十个AI智能体生成约4310万行Lean代码完成形式化