人类历史上规模最大的数学证明，已经通过计算机形式化验证。
Axiom 表示，有限单群分类定理（CFSG，Classification of Finite Simple Groups）已被其多智能体系统完整形式化。围绕这一结果，团队称，约 100 位数学家自 1950 年代起在 500 多篇论文中累积写下约 15000 页证明，如今在 24 天内被转换并跑通为 Lean 代码库。
被称为「巨型定理」的分类工程
在数学界，有限单群分类定理长期被称为「巨型定理」（The Enormous Theorem）。报道提到，在此之前，没有任何一个人能够从头到尾完整通读它的全部证明。
群论用于描述对称性。按文中解释，有限群可以像化学分子分解为原子一样，被拆解为不可再分的「基本构件」，也就是有限单群。分类定理的核心结论，是为这些基本构件给出完整分类。
文中列出的分类包括：素数阶循环群、至少 5 个符号的交错群、16 个无限家族的李型群，以及 26 个无法归类的零散群。其中最大的零散群被称为「魔群」（Monster Group）。
报道还提到，1998 年，Richard Borcherds 因证明「怪兽月光猜想」获得菲尔兹奖；2007 年，Edward Witten 提出，包含魔群的理论可能被用于描述一个简化宇宙中的引力，并用于编码黑洞在不同能级上的量子态分布，从而计算黑洞熵。
这套证明体系的形成持续了数十年。按原文说法，从 1950 年代开始，大约 100 位数学家在 500 多篇学术论文中拼接出约 15000 页证明，篇幅约相当于 14 部《红楼梦》。
但它并非一次性完成。1983 年，Gorenstein 宣布证明完成时，仍留下一个巨大缺口，直到 2004 年才由 Aschbacher 和 Smith 用 1221 页论文补上。Aschbacher 的一句话也被原文引用：「要写出一个非常长且复杂的论证而不犯错，是不可能的。」
AxiomProver 在 24 天内生成 4310 万行 Lean 代码
面对这套 1.5 万页证明，Axiom 没有采用文中所称的传统蛮力计算方式，而是使用多智能体系统 AxiomProver，将自然语言证明翻译为 Lean 代码，也就是形式化证明。
按报道给出的时间线，2026 年 10 月 1 日，Axiom 团队在一个 Slack 频道中启动项目。人类工程师和数学家先将整个「巨型定理」拆成 108 个里程碑和约 380 个小任务，形成一张证明地图。10 月 2 日，第一批 AI 智能体上线。
这些智能体分工协作：有的负责拆解高难度论证，有的搜索现有结果，有的编写 Lean 代码；如果遇到尚未证明的前提条件，系统会把任务继续分派给其他智能体，最终结果汇总到共享代码库。
过程中也出现了工程瓶颈。报道称，由于 AI 生成代码速度过快，Lean 在重新检查依赖项时出现算力瓶颈，Axiom 工程师随后临时重构底层基础设施，并开发分布式缓存系统，以跟上代码产出速度。
10 月 10 日，Slack 频道出现一条消息：「我们证明了魔群是单群。」报道称，AI 不仅从结构信息中识别出魔群，还通过代码形式化了它的存在。
24 天后，AxiomProver 共产出 4310 万行 Lean 代码。按原文表述，这构成了人类目前最大的 Lean 代码库；若按代码行数计算，它也被描述为史上最大的开源软件项目，规模超过 Linux 内核、Chromium、Firefox、LLVM、GCC 和 FFmpeg。
形式化过程中发现数百处异常，34 处被列为重大逻辑偏差
形式化证明要求每一步都具备明确逻辑支撑。原文以数学论文中常见的「显然可得」「同理可证」「易证」为例，说明这类省略在人类写作中常见，但在形式化系统中无法直接通过。
按报道说法，AxiomProver 在逐行扫描和强迫推理过程中记录了数百处异常。其中大部分被描述为笔误、表格错误或前提条件遗漏，另有 34 处属于重大逻辑偏差。
最关键的问题出现在不平衡群定理（UGT，Unbalanced Group Theorem）。报道称，UGT 是整个分类定理中的关键环节，其作用是通过研究一个群的子群结构，推断整个大群的性质。
Axiom 团队最初采用 John Walter 于 1986 年发表的一篇权威文献作为形式化基础。但在翻译这部分论证时，AI 智能体发现 Walter 证明中的一个关键闭包断言在逻辑上无法成立。
系统不仅指出问题，还给出一个明确反例：PSL₂(49)。按原文描述，在这个反例中，一个操作会产生一个被明确排除在目标家族之外的群，因为 7 是梅森素数。报道将这一发现描述为整套 15000 页逻辑体系面临断链风险。
Richard Lyons 与 Ronald Solomon 参与修补，AI 完成新定理证明
面对这一漏洞，Axiom 团队没有转向后续版本的「第二代证明」，因为报道称那会引入大量新依赖，并可能让此前 24 天的工作失效。
随后，团队联系了曾参与 CFSG 原始工作的 Richard Lyons 和 Ronald Solomon。报道称，在听取 AI 发现的问题后，数学家基于 Solomon 于 1976 年提出的理论，构思出一条新的证明路线。
在这一路线下，AxiomProver 证明了一个新的群论结果：Preservation of simple tops。原文将其描述为一块定制补丁，用来填补人类证明中留下的缺口，并成功推出分类定理所需的 UGT 形式。
报道据此称，定理本身依然成立，但证明已不再完全属于人类。这也是原文所称，AI 首次在顶级纯数学研究中不只是充当验算工具，还参与发现新定理并修补核心漏洞。
Ken Ono 发文纪念父亲
原文还提到，数学家 Ken Ono 就这一进展发文，并悼念于今年 1 月去世的数学家父亲。他回忆童年时期在父亲引荐下接触群论大师的经历，并在见证人机协作跨过这一节点时落泪。
报道同时提到另一段数学史案例。2002 年菲尔兹奖得主 Vladimir Voevodsky 曾发现自己的证明存在错误且无法修复。按原文说法，他在 1999 至 2000 年于普林斯顿高等研究院讲课时，发现早年关键引理有误；2013 年又确认 1989 年另一项结果也存在错误，而相关反例早在 1998 年就已出现。此后，他转向 Coq、同伦类型论与单值基础，希望借助计算机检验数学证明。
本文援引的参考资料包括 Ken Ono 在 X 平台发布的内容，以及 Axiom 官网研究页面《The Enormous Theorem Formalized》。原文署名显示，文章来自微信公众号「新智元」，作者为「ASI启示录」。
