AI补全人类史上最大数学证明，数学家当场泪崩

　　新智元报道

　　人类历史上规模最大的数学证明，现已通过计算机形式化验证。

　　有限单群分类定理（CFSG，Classification of Finite Simple Groups），刚刚被 AI 彻底形式化！

　　百余名全球顶尖数学家历经大半个世纪、写下长达 15000 页的「数学天书」，被初创团队 Axiom 研发的多智能体系统在短短 24 天内全部跑通。

　　更让人头皮发麻的是，AI 构建了人类史上首个超 4000 万行的 Lean 代码库。

　　按代码行数计算，这现在是史上最大的开源软件项目。它的规模超过了 Linux 内核、Chromium、Firefox、LLVM、GCC、FFmpeg 等。

　　它甚至还在原有的证明中揪出了人类的漏洞，并亲自证明了新的数学定理来完成修补！

　　知名数学家 Ken Ono 动情发文，悼念今年 1 月去世的数学家父亲。

　　他回忆起童年时父亲引荐自己走近群论巨匠的岁月，在见证人机协作跨过这条历史终点线时，这位数学大师忍不住当场泪崩。

　　数学的「对称周期表」：巨型定理

　　在数学界，这个定理有一个如雷贯耳的绰号——「巨型定理」（The Enormous Theorem）。

　　在此之前，世界上没有任何一个人能够从头到尾完整通读它的所有证明。

　　到底什么是「群」？

　　简单来说，群是描述「对称性」的数学语言。

　　比如，描述正六边形的对称性，对应一个二面体群群：

　　比如，用图论看魔方，每个状态是一个顶点，每一步移动是这张巨大图中的一条边。

　　这段动画展示了排列如何穿越 43 百亿亿种配置，最终抵达解法。

　　而所有的有限群，都可以像化学分子被分解为原子一样，被分解为不可再分的「基本构件」——这就是有限单群（Finite Simple Groups）。

　　分类定理的伟大之处就在于，它为全宇宙的对称性开列了一张「元素周期表」。

　　它明确宣告：

　　所有的有限单群，要么属于素数阶循环群，要么属于至少 5 个符号的交错群，要么属于 16 个无限家族的李型群，要么，就属于 26 个极度特殊、无法归类的「零散群」（Sporadic groups）。

　　这 26 个零散群中，最大的一个被数学家敬畏地称为「魔群」（Monster Group）。

　　顺便提一句，1998 年，Richard Borcherds 因证明著名的「怪兽月光猜想」（Monstrous Moonshine），荣获菲尔兹奖 。这一猜想揭示了数学中一个令人震惊的联系：最大的散在单群「魔群」，竟然与数论中的模函数存在深刻的数学关联。

　　2007 年，物理学巨擘 Edward Witten 更是提出，这套包含魔群的理论，可能被用来描述一个简化宇宙中的引力，用来编码黑洞在不同能级上的量子态分布，从而计算黑洞的熵！

　　从 1950 年代开始，为了证明巨型定理，大约 100 位数学家在 500 多篇学术论文中，拼凑出了长达 15000 页的证明，约 14 部《红楼梦》。

　　它太庞大、太分散了，以至于 1983 年数学家 Gorenstein 宣布证明完成时，其实还漏掉了一个巨大的缺口，直到 2004 年才由 Aschbacher 和 Smith 用 1221 页的论文补上。

　　因为证明实在太长，人类极容易出错。正如 Aschbacher 所言：「要写出一个非常长且复杂的论证而不犯错，是不可能的。」

　　既然人类的大脑已经逼近处理复杂逻辑的极限，那么，是时候让 AI 登场了。

　　AI 出征：24 天，干了人类半个世纪的活

　　面对这座 1.5 万页的「数学珠穆朗玛峰」，Axiom 团队没有选择传统的蛮力计算，而是动用了多智能体蜂群——AxiomProver。

　　把人类的自然语言证明翻译成 Lean 代码（即「形式化」），就等同于让一台铁面无私的机器，用放大镜去检验那 15000 页纸上的每一个标点符号。

　　2026 年 10 月 1 日，Axiom 团队在一个 Slack 频道里敲下了启动的指令。

　　人类工程师和数学家将庞大的「巨型」拆解成 108 个里程碑和约 380 个小任务，生成了一张巨大的「证明地图」。

　　10 月 2 日，第一批 AI「蜂群」正式上线。

　　这群 AI 智能体像一支训练有素的军队一样开始分工协作。领头的 AI 负责拆解高难度的论证，其他 AI 则疯狂搜索现有结果或埋头编写 Lean 代码。如果一个 AI 遇到了还没证明的先决条件，它会自动把这个任务外包给另一个 AI。所有的结果都会汇聚到一个共享的代码库中。

　　整个过程并非一帆风顺。由于 AI 编写代码的速度实在太快，Lean 系统在重新检查依赖项时甚至出现了算力瓶颈。

　　Axiom 的工程师不得不临时重构底层的工程基础设施，开发了一套分布式缓存系统，才勉强跟上 AI 那恐怖的产出速度。

　　10 月 10 日，Slack 频道里弹出了一条让所有人沸腾的消息：

　　我们证明了魔群是单群。

　　AI 不仅从结构信息中识别出了魔群，还通过代码彻底形式化了它的存在！

　　仅仅 24 天！

　　在 24 个日日夜夜里，这群不知疲倦的 AI 智能体，产出了惊人的4310 万行Lean 代码，构建了人类目前最大的 Lean 代码库。

　　人类的智慧，经过了机器无情的检验，而且发现了其中的逻辑漏洞！

　　史诗级反转：AI 揪出人类大师的「致命 Bug」并亲手修复

　　人类的语言总是充满省略。

　　有网友做词一首，调侃数学证明中的思维跳跃：

　　西江月·证明

　　即得易见平凡，仿照上例显然

　　留作习题答案略，读者自证不难

　　反之亦然同理，推论自然成立

　　略去过程 Q.E.D.

　　由上可知证毕

　　「显然可得」、「同理可证」、「易证」……这些数学论文里常见的词语，对 AI 来说却是行不通的。

　　形式化证明要求每一步都必须有明确的逻辑支撑。

　　在逐行扫描、强迫推理的过程中，AI 智能体记录下了数百处异常。其中大部分是人类的笔误、表格错误或遗漏了前提条件，但有34 处是重大的逻辑偏差！

　　而其中最惊险、最核心的一个「Bug」，出在至关重要的不平衡群定理（Unbalanced Group Theorem, UGT）上。

　　UGT 是整个分类定理中极为关键的一环，它的作用是「通过局部看整体」——通过研究一个群的子群结构，来推断出整个大群的真面目。

　　Axiom 团队最初选择了 John Walter 在 1986 年发表的一篇权威文献作为形式化的基础。

　　然而，在翻译这段人类自以为完美无缺的论证时，AI 智能体突然发出了红色警报！

　　AI 发现，Walter 证明中的一个关键闭包断言，在逻辑上是站不住脚的。

　　AI 不仅指出了错误，还给出了一个明确的反例：PSL₂(49)。在这个反例中，一个操作会产生一个被明确排除在目标家族之外的群（因为 7 是梅森素数）。

　　人类引以为傲的证明，在这一刻断链了。

　　长达 1.5 万页的逻辑大厦，随时面临崩塌的危险。

　　怎么办？如果去借用后人写的「第二代证明」，不仅会引入海量的全新依赖，还会让这 24 天的努力前功尽弃。

　　此时，人机协作的巅峰一幕上演了。

　　Axiom 团队紧急连线了当年参与 CFSG 原始工作的活化石——群论泰斗 Richard Lyons 和 Ronald Solomon。

　　在听取了 AI 发现的漏洞后，人类大师的直觉与 AI 的算力展开了完美共振。基于 Solomon 在 1976 年提出的理论，人类数学家构思出了一条新的证明路线。

　　随后，AxiomProver（AI 系统）亲自上阵，根据新思路，严丝合缝地证明了一个全新的群论结果——Preservation of simple tops。

　　这个由 AI 主导证明的新定理，像一块完美的定制补丁，精准地填补了人类大师当年留下的窟窿，成功推导出了分类定理所需的 UGT 形式！

　　定理依然成立，但证明已经不完全属于人类了。

　　这是人类历史上第一次，AI 在最顶级的纯数学研究中，不仅充当了「验算器」，更成为了发现新定理、修补核心漏洞的「合作研究员」！

　　这不禁让人想起数学史上类似的一幕：2002 年菲尔兹奖得主 Vladimir Voevodsky，发现自己的证明是错的，而且救不回来。

　　1999–2000 年，在普林斯顿高等研究院讲课时，他发现早年关键引理有误，原命题无法按原样挽救。

　　2013 年又确认 1989 年另一项结果也错了——反例早在 1998 年就有人提出。

　　他不再相信人类能可靠地检查复杂证明，转向 Coq、同伦类型论与单值基础：让计算机验数学。

　　在追求数学真理的道路上，人类用血肉之躯和有限的大脑，进行了长达近两百年的悲壮远征。

　　如今，人类有了新的合作伙伴，一起探索知识疆域的星辰大海。

　　参考资料：

　　https://x.com/KenOno691/status/2115090084861247680

　　https://axiommath.ai/research/the-enormous-theorem-formalized/

　　编辑：大卫