人类历史上规模最大的数学证明——有限单群分类定理（CFSG），首次被AI完整形式化验证。Axiom团队研发的多智能体系统AxiomProver在24天内，将百余名数学家耗时半个多世纪写成的15000页证明翻译成Lean代码，并构建了超过4000万行的代码库，按行数计已成为史上最大的开源软件项目，规模超过Linux内核、Chromium、Firefox等。

CFSG在数学界被称为「巨型定理」，它像一张对称性的元素周期表，宣告所有有限单群要么属于素数阶循环群、交错群、李型群，要么属于26个零散群，其中最大的是「魔群」。该证明从1950年代开始，约100位数学家在500多篇论文中拼凑完成，1983年宣布完成时还漏掉一个巨大缺口，直到2004年才用1221页论文补上。由于证明太长，人类几乎无法避免错误。

Axiom团队没有采用蛮力计算，而是将证明拆解为108个里程碑和约380个小任务，由多个AI智能体分工协作：领头的AI拆解高难度论证，其他AI搜索现有结果或编写Lean代码，遇到未证明的先决条件自动外包给另一个AI。由于AI产出速度过快，Lean系统重新检查依赖项时出现算力瓶颈，工程师不得不开发分布式缓存系统才跟上节奏。10月10日，AI成功证明了魔群是单群。

更关键的是，AI在逐行扫描中记录了数百处异常，其中34处是重大逻辑偏差。最核心的一处出现在不平衡群定理（UGT）上：AI发现John Walter在1986年论文中的一个关键闭包断言逻辑不成立，并给出反例PSL₂(49)。Axiom团队紧急联系当年参与CFSG工作的群论泰斗Richard Lyons和Ronald Solomon，人类数学家基于Solomon在1976年的理论构思新路线，随后AxiomProver亲自证明了一个全新群论结果——Preservation of simple tops，精准填补了漏洞。

这是AI首次在顶级纯数学研究中不仅充当验算器，更成为发现新定理、修补核心漏洞的合作研究员。知名数学家Ken Ono在见证人机协作跨过终点线时动情落泪，悼念今年1月去世的数学家父亲。这一事件也呼应了数学家Vladimir Voevodsky因发现自身证明有误而转向计算机验证的往事，暗示数学研究的人机协作时代正在加速到来。