重磅，AI补全人类史上最大数学证明，数学家当场泪崩 - 6686体育

人类历史上规模最为宏大的数学证明，如今已通过计算机手段完成了形式化验证。

有限单群分类定理，已被AI系统彻底形式化！

超过一百位全球顶尖数学家耗费大半个世纪、汇编成15000页的“数学巨著”，被创业团队Axiom研发的多智能体系统在仅仅24天内全部完成。

更令人震撼的是，AI构建了人类历史上首个超过4000万行的Lean代码库。

按照代码行数计算，这已成为史上最大的开源软件项目。它的规模超越了Linux内核、Chromium、Firefox、LLVM、GCC、FFmpeg等知名项目。

它甚至在原有证明中发现了人类的错误，并自行证明了新的数学定理来完成修复！

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

他回忆起童年时父亲引导自己接触群论大师的日子，在目睹人机协作跨越这条历史性终点线时，这位数学大家忍不住当场落泪。

数学的“对称周期表”：巨型定理

在数学界，这个定理有一个响亮的别名——“巨型定理”。

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

究竟什么是“群”？

简单而言，群是描述“对称性”的数学语言。

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

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

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

而所有的有限群，都可以像化学分子被分解为原子一样，被分解为不可再分的“基本构件”——这就是有限单群。

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

它明确宣告：

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

这26个零散群中，最大的一个被数学家敬畏地称为**“魔群”**。

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

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”，出在至关重要的不平衡群定理上。

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亲自上阵，根据新思路，严丝合缝地证明了一个全新的群论结果——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/

本文来自微信公众号 “新智元”（ID：AI_era），作者：ASI启示录，36氪经授权发布。