Axiom 24天形式化人类最长数学证明 4310万行

时间：2026年10月30日，这是中文 AI 媒体集中报道这条消息的日子；Axiom Math 的官方公告发布于 10 月 26 日，配套预印本论文于 10 月 27 日上传。 地点：Axiom Math 团队的在线协作环境，全部工作通过一个 Slack 频道和一个 GitHub 仓库推进，Lean 证明代码托管在 GitHub 的 AxiomMath/CFSG 仓库里。 人物：Axiom Math 首席研究员 Letong Hong、核心贡献者 Dean Cureton，创始数学家 Ken Ono 与数学贡献者 Colin Defant 是新论文《The Unbalanced Group Theorem》的署名作者；外部顾问包括参与原始分类定理工作的群论泰斗 Richard Lyons 和 Ronald Solomon。 事件详情：Axiom Math 宣布，有限单群分类定理（CFSG）出现了人类历史上第一份完整的计算机核验证明。公司用 Lean 这门能让机器逐步检查每一步的证明语言，重写了这条被称为“巨型定理”的论证，由数十个 AI 智能体组成的 AxiomProver 蜂群完成。人类原始证明散落在约 500 篇论文、约 15000 页之中，由上百位数学家接力半个世纪写成，从未有人从头到尾通读过全部材料。Axiom 团队 10 月 1 日开设 Slack 频道启动项目，10 月 2 日第一批智能体上线，把工作拆成 108 个里程碑和约 380 个子任务，智能体各自认领任务、把论文翻译成 Lean 代码，缺前置条件就外包给别的智能体。24 天里蜂群产出约 4310 万行 Lean 代码，10 月 10 日频道里出现了一句“WE PROVED MONSTER IS SIMPLE”，证明最大的散在单群“魔群”确实是单群。形式化过程中还查出 34 处与已发表文献的显著偏差，最关键的一处出在不平衡群定理（UGT）上：AI 在 John Walter 1986 年的论证里发现一条闭包断言站不住脚，并给出明确反例 PSL₂(49)，但这并没有推翻 UGT 本身。与 Lyons、Solomon 讨论后，基于 Solomon 1976 年的最大 2-元分支理论，AI 自己证明出一个新的群论结果“单顶保持定理”（论文中的 Theorem 2.3），把缺口补上，团队随后还找到一条适配第一代证明的更短路径，两套方案都写进了配套论文。 背景：分类定理的来历横跨半个多世纪，19 世纪 Galois 与 Jordan 起步，1983 年 Gorenstein 宣布证明完成却留下一个巨大缺口，直到 2004 年 Aschbacher 与 Smith 用 1221 页专著补齐，才有了“第一代证明”，结构更简洁的“第二代证明”至今没有写完，这次形式化因此选了第一代证明作蓝本。2012 年 Georges Gonthier 团队用 Coq（现改称 Rocq）花六年完成费特-汤普森定理的形式化，这是人类第一次把这种量级的定理整体交给机器检查，Aschbacher 早在 2005 年就写下过一句判断：写出很长的复杂论证而不出错，几乎不可能。分类定理把所有有限单群分成素数阶循环群、至少 5 个符号的交错群、16 类李型群和 26 个散在群，魔群约有 8×10⁵³ 个元素，Borcherds 靠“怪兽月光猜想”拿到 1998 年菲尔兹奖，Witten 在 2007 年还提出这套理论可能用来描述黑洞的量子态分布。这次的形式化站在社区既有成果之上，复用了 Mathlib 以及 Qiuzhen-CFSG 约 120 万行已有代码。 影响：这是第一次 AI 不只是扮演“验算器”，而是在顶级纯数学里挑出人类论证的漏洞、给出反例、再自己证明一个新定理去修补，新智元评论说“定理依然成立，但证明已经不完全属于人类了”。4310 万行 Lean 代码按行数算已经超过 Linux 内核、Chromium、Firefox、LLVM 等主流开源项目，新智元称其为史上最大的开源软件项目，勘误表、依赖关系图谱、代码仓库和修复论文全部公开，任何人都能逐行复核。同时它也提醒了一件事：分类定理的数学结论仍然是上百位群论学者的集体智慧，Axiom 的贡献是让它可被机器检查、让潜藏的缺口显性化，并给出可复现的修复方案。代数、数论、组合论和理论物理里大量直接引用分类定理的论文，从此多了一份可机检的依赖版本，研究者可以精确追踪每条推论背后的前提条件。 总结：24 天、4310 万行 Lean 代码，人类花了半个世纪、写了约 15000 页的最长证明，第一次有了完整的机器核验版本。真正的突破点不是算得多快，而是形式化把“显然可得”“同理可证”这类人类省略全部逼成了显式步骤，于是人类的漏洞无处可藏。AI 在其中已经不只是验证工具，而是能发现错误、给出反例、写出补丁的合作研究者。对做 AI 的人来说，这件事更直接的意义在于，形式化验证工具链正在从数学家的专业工具变成 AI 研究的标准动作。 常见问题： 问：AI 证明和人类证明有何不同？ 答：人类证明允许“显然可得”这类省略，形式化要求每步可被机器检查，这次就查出 34 处文献偏差。 问：这次证明了几个定理？ 答：主体是 1 个有限单群分类定理；AI 还新证明了“单顶保持定理”补缺口。 问：4310 万行 Lean 代码有多大？ 答：按行数已超过 Linux 内核、Chromium 等项目，新智元称它是史上最大的开源软件项目。 参考来源： Axiom Math 官方博客《Formalizing the Enormous Theorem》，10 月 26 日发布的官方公告 https://axiommath.ai/research/the-enormous-theorem-formalized/ 预印本《The Unbalanced Group Theorem》，作者 Colin Defant、Ken Ono，10 月 27 日版本 1 https://hexagonmath.org/2610.00575?version=1 36 氪转载新智元《重磅，AI补全人类史上最大数学证明，数学家当场泪崩》，10 月 30 日 https://www.36kr.com/p/4048319038208262 DoNews《Axiom 完成巨大定理全球首份完整机器核验证明》，10 月 29 日 https://www.donews.com/news/detail/1/6757781.html Axiom Math 官方证明站，含证明地图与勘误表 https://cfsg.axiommath.ai/ GitHub 上的 Lean 形式化代码仓库 AxiomMath/CFSG https://github.com/AxiomMath/CFSG 数学家 Ken Ono 关于该成果的推文 https://x.com/KenOno691/status/2115090084861247680 意大利数学博客 maddmaths 对该成果的解读文章 https://maddmaths.simai.eu/ricerca/mathai/je-nai-pas-le-temps-ma-lia-si-il-teorema-enorme-43-milioni-di-righe-e-qualche-sorpresa/