AI补全最大数学证明

人类历史上规模最大的数学证明，现已通过计算机形式化验证。 有限单群分类定理（CFSG），刚刚被AI彻底形式化！ 百余名全球顶尖数学家历经大半个世纪、写下长达15000页的「数学天书」，被初创团队Axiom研发的多智能体系统在短短24天内全部跑通。 AI构建了人类史上首个超4000万行的Lean代码库，按代码行数计算，这现在是史上最大的开源软件项目。 它甚至还在原有的证明中揪出了人类的漏洞，并亲自证明了新的数学定理来完成修补！

知名数学家Ken Ono动情发文，悼念今年1月去世的数学家父亲，在见证人机协作跨过这条历史终点线时，这位数学大师忍不住当场泪崩。 在数学界，这个定理有一个如雷贯耳的绰号——「巨型定理」（The Enormous Theorem）。 「群」是描述「对称性」的数学语言，有限群可以被分解为不可再分的「基本构件」——有限单群。 分类定理的伟大之处在于，它为全宇宙的对称性开列了一张「元素周期表」。

所有的有限单群，要么属于素数阶循环群，要么属于至少5个符号的交错群，要么属于16个无限家族的李型群，要么，就属于26个极度特殊、无法归类的「零散群」（Sporadic groups）。 这26个零散群中，最大的一个被数学家敬畏地称为「魔群」（Monster Group）。 从1950年代开始，为了证明巨型定理，大约100位数学家在500多篇学术论文中，拼凑出了长达15000页的证明。 因为证明实在太长，人类极容易出错。 既然人类的大脑已经逼近处理复杂逻辑的极限，那么，是时候让AI登场了。

Axiom团队没有选择传统的蛮力计算，而是动用了多智能体蜂群——AxiomProver。 把人类的自然语言证明翻译成Lean代码（即「形式化」），就等同于让一台铁面无私的机器，用放大镜去检验那15000页纸上的每一个标点符号。 2026年10月1日，Axiom团队在一个Slack频道里敲下了启动的指令。 人类工程师和数学家将庞大的「巨型」拆解成108个里程碑和约380个小任务，生成了一张巨大的「证明地图」。 10月2日，第一批AI「蜂群」正式上线。 这群AI智能体像一支训练有素的军队一样开始分工协作。

整个过程并非一帆风顺。 由于AI编写代码的速度实在太快，Lean系统在重新检查依赖项时甚至出现了算力瓶颈。 Axiom的工程师不得不临时重构底层的工程基础设施，开发了一套分布式缓存系统，才勉强跟上AI那恐怖的产出速度。 10月10日，Slack频道里弹出了一条让所有人沸腾的消息：我们证明了魔群是单群。 仅仅24天！ 在24个日日夜夜里，这群不知疲倦的AI智能体，产出了惊人的4310万行Lean代码，构建了人类目前最大的Lean代码库。 人类的智慧，经过了机器无情的检验，而且发现了其中的逻辑漏洞！

人类的语言总是充满省略，形式化证明要求每一步都必须有明确的逻辑支撑。 在逐行扫描、强迫推理的过程中，AI智能体记录下了数百处异常。 其中大部分是人类的笔误、表格错误或遗漏了前提条件，但有34处是重大的逻辑偏差！ 而其中最惊险、最核心的一个「Bug」，出在至关重要的不平衡群定理（UGT）上。 Axiom团队最初选择了John Walter在1986年发表的一篇权威文献作为形式化的基础。 然而，在翻译这段人类自以为完美无缺的论证时，AI智能体突然发出了红色警报！

AI发现，Walter证明中的一个关键闭包断言，在逻辑上是站不住脚的。 AI不仅指出了错误，还给出了一个明确的反例：PSL₂(49)。 在这个反例中，一个操作会产生一个被明确排除在目标家族之外的群。 人类引以为傲的证明，在这一刻断链了。 此时，人机协作的巅峰一幕上演了。 Axiom团队紧急连线了当年参与CFSG原始工作的活化石——群论泰斗Richard Lyons和Ronald Solomon。 在听取了AI发现的漏洞后，人类大师的直觉与AI的算力展开了完美共振。

基于Solomon在1976年提出的理论，人类数学家构思出了一条新的证明路线。 随后，AxiomProver（AI系统）亲自上阵，根据新思路，严丝合缝地证明了一个全新的群论结果——Preservation of simple tops。 这个由AI主导证明的新定理，像一块完美的定制补丁，精准地填补了人类大师当年留下的窟窿，成功推导出了分类定理所需的UGT形式！ 定理依然成立，但证明已经不完全属于人类了。

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