1.5万页人类最大数学证明被AI形式化：4310万行代码揪出潜伏40年的漏洞

人类数学史上最庞大的一套证明，有一万五千页。 五百多篇论文，一百多位顶尖学者，前前后后写了半个世纪。 更绝的是，整个人类数学界，从来没有一个人能把它从头到尾完全读完。 大家只能互相相信对方的论文没毛病。 这个东西叫有限单群分类。 数学家管它叫对称性的元素周期表。 宇宙里所有的对称结构，拆到最后，全由这几种最基本的积木拼出来。 从上世纪八十年代起，大家就默认它已经证明完了。 但谁心里都清楚，一万五千页的纸堆里，肯定藏着人类眼皮子底下的错漏。 谁来复查呢？ 没人有这个脑容量，也没人有这几个几十年的寿命。 结果上个月，一群 AI 智能体把这套巨型证明给啃完了。 用的是形式化数学工具 Lean 4。 二十四天。 四千三百一十万行代码。 两百零五万个数学声明。 最精彩的一幕来了。 当智能体一行一行把论文翻成计算机代码时，机器突然卡住报警了。 它指着 1986 年数学家约翰·沃尔特写的一篇经典论文说：这里逻辑断了。 那是关于非平衡群定理的核心步骤。 作者在论文里顺理成章地写了一个闭包断言，觉得某种子群算下来一定跑不出原本的范围。 过去四十年，所有读到这里的数学家都点头放行了。 因为看起来太自然、太合理了。 结果机器死活通不过。 AI 抓出了一个具体的反例：四十九元有限域上的射影特殊线性群，代号 PSL₂(49)。 只要一撞上这个群，原本以为关在笼子里的东西，直接就跳出来了。 一个在数学界核心文献里躺了整整四十年的漏洞，就这么被揪了出来。 更离谱的是，AI 没有直接撂挑子。 它配合研究团队，调出了罗纳德·所罗门 1976 年关于极大二分量的老理论。 顺着这个思路，硬生生补出了一个新的替代定理，写了三十五页补充证明。 然后把代码缝了回去。 整个证明工程跑下来，机器一共找出了人类文献里的三十四个漏洞和疏漏。 大部分是漏了假设条件或者笔误，只有这一处是真正的逻辑断档。 最后，微内核全部验证通过。 在 Lean 语言里，如果你不会证或者想跳过一步，代码里可以写一个词叫 sorry。 只要留了一个 sorry，整条链条就算作弊。 这四千三百一十万行代码里，一个 sorry 都没有。 这是人类第一次用计算机，把一万五千页的数学丛林彻底给推平了。 以前我们总觉得数学是纯粹理性的象牙塔。 可当证明的体量膨胀到一万多页，整件事早就变成了同行之间半凭直觉、半凭信任的经验科学。 人类的大脑会被疲劳击垮，会被权威的名气说服，会默认大师写的一定严丝合缝。 但机器不管你是谁。 在微内核的类型检查面前，没有面子，没有差不多，也没有四十年没人怀疑的惯性。 它就坐在那，面无表情地看着你。 只要逻辑里差了一块拼图，它就永远不给你敲回车。