AI用24天形式化15000页数学巨著，数学家当场泪崩

人类历史上规模最大的数学证明已通过计算机形式化验证。有限单群分类定理（CFSG）被AI彻底形式化：百余名全球顶尖数学家历经大半个世纪、写下长达15000页的证明，被初创团队Axiom研发的多智能体系统在24天内全部跑通。AI构建了人类史上首个超4000万行的Lean代码库，按代码行数计算是史上最大的开源软件项目，规模超过Linux内核、Chromium、Firefox、LLVM、GCC、FFmpeg等。它还在原有证明中揪出人类漏洞，并证明新定理完成修补。

有限单群分类定理被称为“巨型定理”。群是描述对称性的数学语言，所有有限群都可分解为不可再分的“基本构件”——有限单群。分类定理为全宇宙的对称性开列了一张“元素周期表”：所有有限单群要么属于素数阶循环群，要么属于至少5个符号的交错群，要么属于16个无限家族的李型群，要么属于26个极度特殊的“零散群”。其中最大的是“魔群”。1998年Richard Borcherds因证明“怪兽月光猜想”获菲尔兹奖；2007年Edward Witten提出该理论可能用于描述简化宇宙中的引力、计算黑洞熵。

从1950年代开始，约100位数学家在500多篇论文中拼凑出长达15000页的证明。1983年Gorenstein宣布证明完成时还漏掉一个巨大缺口，直到2004年才由Aschbacher和Smith用1221页论文补上。Aschbacher曾言：“要写出一个非常长且复杂的论证而不犯错，是不可能的。”

Axiom团队动用多智能体蜂群AxiomProver，将自然语言证明翻译成Lean代码。2026年10月1日团队启动项目，将“巨型”拆解成108个里程碑和约380个小任务，生成“证明地图”。10月2日第一批AI蜂群上线，分工协作：领头AI拆解高难度论证，其他AI搜索现有结果或编写Lean代码；遇到未证明的先决条件则自动外包给另一个AI，结果汇聚到共享代码库。由于AI写代码速度太快，Lean系统出现算力瓶颈，工程师不得不开发分布式缓存系统。10月10日，团队宣布证明了魔群是单群。24天内AI产出4310万行Lean代码。

形式化证明要求每一步都有明确逻辑支撑。AI在扫描中记录数百处异常，大部分是笔误、表格错误或遗漏前提，但有34处是重大逻辑偏差。最核心的Bug出在不平衡群定理（UGT）上，该定理通过研究子群结构推断大群真面目。团队最初选择John Walter在1986年发表的文献作为形式化基础，但AI发现其中关键闭包断言逻辑上站不住脚，并给出反例PSL₂(49)。Axiom团队紧急连线当年参与CFSG原始工作的群论泰斗Richard Lyons和Ronald Solomon。基于Solomon在1976年提出的理论，人类数学家构思出新证明路线，随后AxiomProver根据新思路证明了全新群论结果“Preservation of simple tops”，填补了漏洞，成功推导出UGT形式。这是人类历史上第一次，AI在最顶级纯数学研究中不仅充当“验算器”，更成为发现新定理、修补核心漏洞的“合作研究员”。

数学史上曾有类似一幕：2002年菲尔兹奖得主Vladimir Voevodsky发现自己的证明有误且无法挽救，此后不再相信人类能可靠检查复杂证明，转向Coq、同伦类型论与单值基础，让计算机验数学。如今，人类有了新的合作伙伴，一起探索知识疆域。