AI智能体24天完成史上最长数学证明的形式化：有限单群分类定理用4310万行Lean代码验证
· 来源：Axiom
Axiom用数十个AI智能体组成的“集群”，在24天内把原本约1.5万页的有限单群分类定理完整写成可由计算机逐步检查的Lean证明。
数学AI公司Axiom宣布，已在Lean证明助手中完成“有限单群分类定理”（CFSG）的完整形式化，这是该定理第一份由计算机检查的完整证明。CFSG被认为是人类写过的最长数学证明，原始证明分布在500多篇论文中，约1.5万页，由大约100位数学家完成，因此有“巨型定理”之称。
据Axiom介绍，公司的工程师和数学家在24天里指挥数十个AI智能体组成的集群协同工作，最终生成约4310万行Lean代码。Lean是一种可以把数学定义、命题和证明写得足够精确、让计算机逐步核验每一步推理的编程语言。相关代码已在GitHub公开。
有限单群可以理解为有限群的“原子”，分类定理给出了这些基本构件的完整清单，相当于有限对称性的“元素周期表”。它不仅是20世纪数学的重大成就，也与理论物理中的“魔群月光”等问题相关。
形式化过程还暴露出已发表证明中的问题：大部分是笔误、表格错误或遗漏条件等小问题，但有34处需要专门处理的重要偏差，其中最主要的一处与“非平衡群定理”有关，Axiom用自己证明的一个新结果替换了它。公司表示将与相关专家一起公开完整勘误表。
需要注意的是，Lean只能保证每一步逻辑正确，形式化的命题和定义是否准确表达了原定理仍需数学家审查；截至目前，外部团队尚未独立重建这份证明。