15000 页、100 位数学家、50 年：AI 用 24 天跑完了，还顺手补上了人类 40 年前的一个逻辑漏洞
AI飞行客 15000 页、100 位数学家、50 年：AI 用 24 天跑完了，还顺手补上了人类 40 年前的一个逻辑漏洞
先说这个定理有多离谱。
有限单群分类定理（CFSG），数学界给它起了个绰号——”巨型定理”（The Enormous Theorem）。
它干的事是：为全宇宙的对称性开出一张”元素周期表”。明确宣告——所有的有限单群，要么是素数阶循环群，要么是至少 5 个符号的交错群，要么属于 16 个无限家族的李型群，要么属于 26 个极度特殊、无法归类的”零散群”。
那 26 个零散群里最大的一个，数学家敬畏地称它为 “魔群”（Monster Group）。
从 1950 年代开始，大约 100 位数学家在 500 多篇论文里，拼出了 15000 页的证明——约 14 部《红楼梦》。
在此之前，世界上没有任何一个人能够从头到尾完整通读它的所有证明。
太庞大了，也太容易出错。1983 年，数学家 Gorenstein 宣布证明完成时，其实还漏掉了一个巨大的缺口，直到 2004 年才由 Aschbacher 和 Smith 用 1221 页的论文补上。
Aschbacher 自己说过一句话：
> “要写出一个非常长且复杂的论证而不犯错，是不可能的。”
这句话，昨天被 AI 证实了。
24 天，4310 万行代码
Axiom 团队做的事，说穿了很简单：把这 15000 页人类自然语言证明，全部翻译成 Lean 代码，让机器逐行检查。
形式化。每一行逻辑都要有明确的支撑，每一个”显然可得”都要被拆开，”同理可证”必须给出具体的同理路径。
2026 年 10 月 1 日，团队在 Slack 里敲下启动指令。人类工程师和数学家把这座”数学珠穆朗玛峰”拆成 108 个里程碑和约 380 个小任务，画了一张巨大的”证明地图”。
10 月 2 日，第一批 AI 蜂群上线。
分工是这样的：领头的 Agent 负责拆解高难度论证，其他的疯狂搜索现有结果或埋头写 Lean 代码。如果一个 Agent 遇到还没证明的先决条件，它会自动把这个任务外包给另一个 Agent。 所有结果汇聚到共享代码库。
中途还出了个很有意思的插曲：AI 写代码速度太快，Lean 系统在重新检查依赖项时出现了算力瓶颈。 工程师不得不临时重构底层基础设施，开发了一套分布式缓存，才勉强跟得上 AI 的产出速度。
10 月 10 日，Slack 里弹出一条消息：”我们证明了魔群是单群。”
AI 不仅从结构信息中识别出了魔群，还把它的存在彻底形式化了。
24 天，4310 万行 Lean 代码。 这是人类史上最大的 Lean 代码库，按代码行数算，也是史上最大的开源软件项目——规模超过了 Linux 内核、Chromium、Firefox、LLVM、GCC、FFmpeg。
真正的反转：AI 找到了人类大师的”致命 Bug”
但形式化本身不新鲜。真正让我坐直了的是后面这段。
人类的数学语言里充满了省略。网上有首词调侃得很到位：
> 即得易见平凡，仿照上例显然 > 留作习题答案略，读者自证不难
这些”显然可得”、”同理可证”，AI 一个都不认。逐行扫描的过程中，AI 记录了数百处异常。大部分是人类笔误、表格错误、遗漏前提条件。
但其中 34 处，是重大的逻辑偏差。
最惊险的一个，出在不平衡群定理（UGT） 上——这是整个分类定理里极为关键的一环，作用是”通过局部看整体”：研究一个群的子群结构，来推断整个大群的真面目。
Axiom 团队选了 John Walter 1986 年发表的一篇权威文献作为形式化基础。
AI 在翻译这段”人类自以为完美无缺”的论证时，发出了红色警报。
它发现 Walter 证明中的一个关键闭包断言，在逻辑上站不住脚。而且它给出了一个明确的反例：PSL₂(49)——在这个反例中，一个操作会产生一个被明确排除在目标家族之外的群，因为 7 是梅森素数。
长达 15000 页的逻辑大厦，这里断了一根梁。
然后是人类和 AI 最漂亮的一次配合
如果改用后人写的”第二代证明”，会引入海量新依赖，24 天的努力前功尽弃。
所以 Axiom 团队做了个决定：把当年参与 CFSG 原始工作的”活化石”请回来。
群论泰斗 Richard Lyons 和 Ronald Solomon 连线进来，听完 AI 发现的漏洞后，基于 Solomon 1976 年提出的理论，构思了一条全新的证明路线。
然后，AxiomProver 亲自上阵，根据新思路，证明了一个全新的群论结果——Preservation of simple tops。
这个由 AI 主导证明的新定理，像一块完美定制的补丁，精准地填上了人类大师当年留下的窟窿，成功推出分类定理需要的 UGT 形式。
定理依然成立。但证明，已经不完全属于人类了。
这是人类历史上第一次，AI 在最顶级的纯数学研究中不只充当”验算器”——它成了发现新定理、修补核心漏洞的合作者。
为什么这件事比”AI 解出千禧年难题”更重
过去几个月，我们已经习惯了这类新闻：OpenAI 的 722 篇手稿、纳维-斯托克斯、ETH 证伪、Siegel 零点。
那些新闻的模式是：AI 造出一个新证明，人类去看懂它。
这件事的模式完全不同：
人类造出一个证明，AI 去检验它，并在检验中发现了人类的错误，然后人类和 AI 一起把错误补上。
前者是”AI 在前面跑，人类在后面追着理解”。 后者是”AI 是审计员，它发现你四十年前的账本记错了，然后你们一起重做了一页”。
我更看重后者。因为它对应的不是某种碾压，而是一种可持续的分工。
而且这件事有一个特别动人的背景：数学家 Ken Ono 发文悼念今年 1 月去世的数学家父亲，回忆起童年时父亲引荐自己走近群论巨匠的岁月。见证人机协作跨过这条历史终点线时，这位数学大师忍不住当场泪崩。
一个延续了七十年的、三代人的工程，在最后一程由一群不会疲倦的机器陪着走完。
三个判断
第一，”没人能完整读完”这件事，本身就是最强的信号。
《红楼梦》十四倍的篇幅，一百位数学家几代人的积累，人类自己的验证能力早就到极限了。这不是 AI 抢了人的活，是这个活本来就该换一种方式做了。
Voevodsky 的经历就是先例。2002 年菲尔兹奖得主，1999-2000 年在普林斯顿高等研究院讲课时发现早年关键引理有误、原命题无法按原样挽救；2013 年确认 1989 年另一项结果也错了。为什么？因为反例早在 1998 年就有人提出，但没人发现。
他从此不再相信人类能可靠地检查复杂证明，转向 Coq、同伦类型论、单值基础——让计算机验数学。
二十多年后，这条路走到了 CFSG。
第二，”34 处逻辑偏差”这个数字，值得所有做长文档的人警惕。
这个数字不是说人类数学家不严谨。恰恰相反，这批证明已经是被反复检查、反复修补过的。但即便经过了半个世纪的审阅，仍能在形式化过程中暴露 34 处重大偏差。
这说明：人的审核能力，在文档长度超过某个阈值之后，会断崖式下降。 而数学证明不是唯一的长文档——法律合同、芯片设计规范、大型软件架构文档、医疗流程手册，全都在同一个区间里。
第三，AI 在这件事里证明的价值，不是”算得快”，是”不肯跳过”。
人类写证明时会说”显然”。这不是偷懒，是必要的——否则篇幅会爆炸。但”显然”这个词背后，是一个没有被验证的跳跃。
AI 的贡献不是算力，是它不肯相信任何一个”显然”。
而这个特质，在数学之外同样稀缺。
—
*定理：CFSG（有限单群分类定理），100+ 位数学家 / 500+ 篇论文 / 15000 页 / 1950s–2004* *执行方：Axiom（AxiomProver 多智能体系统）* *时间线：2026-10-01 启动 → 10-02 蜂群上线 → 10-10 证明魔群是单群 → 24 天完成* *产出：4310 万行 Lean 代码，人类史上最大 Lean 代码库* *关键发现：34 处重大逻辑偏差，核心为 Walter 1986 年 UGT 证明中的闭包断言，反例 PSL₂(49)* *修补：Lyons & Solomon 构思新路线 → AxiomProver 证明 Preservation of simple tops* *来源：新智元 / 36氪 — axiommath.ai/research/the-enormous-theorem-formalized/*