AI用24天完成15000页数学证明的形式化验证
人类历史上规模最大的数学证明，已被AI完成形式化验证。据虎嗅援引新智元报道，初创团队Axiom研发的多智能体系统AxiomProver，用24天把有限单群分类定理（CFSG）的15000页证明翻译为Lean代码，并建成约4310万行的代码库。
有限单群分类定理在数学界被称为“巨型定理”。它以群论语言描述对称性，宣告所有有限单群要么属于素数阶循环群，要么属于至少5个符号的交错群，要么属于16个无限家族的李型群，要么属于26个无法归类的“零散群”。其中最大的零散群被称为“魔群”。1998年，Richard Borcherds因证明“怪兽月光猜想”获得菲尔兹奖；2007年，Edward Witten提出，相关理论或可用于描述简化宇宙中的引力，并计算黑洞的熵。
这项工作的体量此前已超出个人通读的极限。自20世纪50年代起，约100位数学家在500多篇论文中拼出15000页证明，篇幅约相当于14部《红楼梦》。1983年数学家Gorenstein宣布证明完成时仍留有缺口，直到2004年才由Aschbacher和Smith以1221页论文补齐。Aschbacher曾表示，要写出很长且复杂的论证而不犯错是不可能的。
按照Axiom披露的过程，团队于2026年10月1日启动项目，把整体拆解为108个里程碑和约380个小任务；10月2日首批AI智能体上线，分工拆解论证、检索已有结果并编写Lean代码。由于AI产出速度过快，Lean系统在检查依赖项时出现算力瓶颈，工程师临时搭建分布式缓存系统应对。10月10日，系统完成“魔群是单群”的形式化。24天内共产出4310万行Lean代码，按行数计算已超过Linux内核、Chromium、Firefox、LLVM、GCC、FFmpeg等开源项目。
逐行检验还暴露出人类证明中的问题。AI记录下数百处异常，多数为笔误、表格错误或遗漏前提条件，其中34处属于重大逻辑偏差。最核心的一处出现在不平衡群定理（UGT）上：在把John Walter于1986年发表的文献形式化时，AI发现其中一项关键闭包断言不成立，并给出反例PSL₂(49)。
Axiom团队随后联系了参与CFSG原始工作的群论学者Richard Lyons和Ronald Solomon。基于Solomon在1976年提出的理论，数学家构思出新的证明路线，由AxiomProver完成了新结果“Preservation of simple tops”的证明，补上了UGT所需的形式。报道称，这是AI首次在顶级纯数学研究中不只是充当验算工具，还作为发现新定理、修补漏洞的参与者。
数学家Ken Ono在社交平台发文，回忆童年时父亲引荐自己走近群论巨匠的经历，并在见证人机协作跨过这一节点时当场落泪。报道还提到，2002年菲尔兹奖得主Vladimir Voevodsky曾发现自己的证明有误且难以挽回，此后转向Coq与同伦类型论，主张让计算机验证数学。相关资料发布在Axiom官网研究页面及Ken Ono的社交账号上。
常见问题
AI这次到底完成了哪件事？
AI把人类历史上规模最大的数学证明——有限单群分类定理（CFSG）全部完成了形式化验证。由初创团队Axiom研发的多智能体系统AxiomProver，用24天时间跑通了全球百余名数学家历经大半个世纪、写下的15000页证明。
2026年10月1日，Axiom团队在一个Slack频道里敲下启动指令，人类工程师和数学家把这项庞大工程拆解成108个里程碑和约380个小任务。10月2日第一批AI“蜂群”上线，最终产出4310万行Lean代码，构建出人类目前最大的Lean代码库。按代码行数计算，这已是史上最大的开源软件项目，规模超过Linux内核、Chromium、Firefox、LLVM、GCC、FFmpeg等。
AI是怎么发现人类证明里的漏洞的？
形式化要求每一步都有明确的逻辑支撑，AI在逐行扫描中记录下数百处异常，其中34处是重大的逻辑偏差。最核心的一处出在至关重要的不平衡群定理（UGT）上：团队以John Walter在1986年发表的权威文献作为形式化基础，AI智能体发现其中一处关键闭包断言在逻辑上站不住脚，并给出反例PSL₂(49)。
Axiom团队随后连线当年参与CFSG原始工作的群论学家Richard Lyons和Ronald Solomon。基于Solomon在1976年提出的理论，人类数学家构思出新的证明路线，再由AxiomProver证明了一个全新的群论结果“Preservation of simple tops”，填补了这一缺口，成功推导出分类定理所需的UGT形式。
有限单群分类定理为什么被称为“巨型定理”？
因为它庞大到此前没有任何一个人能够从头到尾完整通读它的所有证明。从1950年代开始，大约100位数学家在500多篇学术论文中，拼凑出长达15000页的证明，体量约相当于14部《红楼梦》。
证明太长，人也极容易出错。1983年数学家Gorenstein宣布证明完成时，其实还漏掉了一个巨大的缺口，直到2004年才由Aschbacher和Smith用1221页论文补上。正如Aschbacher所说：“要写出一个非常长且复杂的论证而不犯错，是不可能的。”这个定理本身则被称为有限群的“元素周期表”，为全宇宙的对称性开列清单。