全世界数学家花了整整八年，才给计算机定理库攒下 220 万行代码

全世界数学家花了整整八年，才给计算机定理库攒下 220 万行代码。 一个由 AI 驱动的系统只用了 11 天，写出了 1300 万行。 它把人类数学史上著名的费马大定理，从头到尾用 Lean 语言形式化证明了一遍。 中间跨越了 29500 个引理，消耗了 60 亿个 Token。 消息一出来，很多人第一反应是怀疑。 大模型最容易一本正经地胡说八道。 1300 万行代码，只要错一个符号全盘皆输，它怎么可能做到零差错跑通？ 还有人以为 AI 自己发明了全新的数学，在惊呼奇点降临。 两种看法都没看清底下运转的那台精密机器。 德布鲁因准则与图前沿调度。 1995 年，安德鲁·怀尔斯证明费马大定理时，论文长达上百页。 哪怕是全世界顶尖的数学家，在同行评审时也要耗费数月甚至数年才能看懂。 当年评审专家尼克·卡茨在手稿里揪出一个隐蔽的逻辑漏洞，怀尔斯闭门重算了 14 个月才把漏洞补齐。 这就是传统数学的瓶颈：人类的信任，建立在极易疲劳的脑力审查上。 为了把这种主观模糊性彻底拔掉，数学界开始用 Lean 语言做形式化验证，把数学推导变成计算机能逐行编译的代码。 帝国理工学院的凯文·巴扎德教授原本带队在做这件事，预估集中全球顶尖学者也得耗费数年工程。 哥伦比亚大学彭天翼团队与 Anthropic，把这个数年的人力活压缩到了 11 天。 秘密就在第一台零件：1968 年荷兰数学家尼古拉斯·德布鲁因立下的「德布鲁因准则」。 这个准则规定：一个计算机证明系统是否可信，只取决于它最底层那个极小、极纯粹的微内核。 外面的 AI 怎么天马行空、生成了多少垃圾草稿，都无关紧要。 只要代码被送进微内核，通过了严格的类型检查，它在逻辑上就是不可推翻的真理。 那个极小的内核，成了阻断大模型一切幻觉的物理滤网。 AI 不需要保证自己永不犯错，它只需要像发电机一样疯狂生成推演候选。 内核会把 99% 的错误答案直接扔掉，只把通过检查的真理盖章放行。 但如果只靠单台 Agent 蛮干，面对费马大定理这种跨越数论、代数几何的庞然大物，上下文窗口很快就会崩溃，Agent 之间也会陷入混乱死锁。 这就轮到了第二台零件：Prove2Me 架构下的「图前沿调度」。 怀尔斯的证明被拆解成了一张由数万个定理构成的有向无环图。 每一个定理需要哪些前置引理，依赖关系全部锁定。 上百个 Agent 蜂群被派到这张拓扑图的最前沿去接单。 只要一个定理的前置条件被微内核全部敲章确认，这个节点就变成了一块不可修改的公共积木。 Agent 永远只在最前沿认领那些刚刚就绪的任务。 只要一个引理被证明，下游的通路立刻被点亮，供下一批 Agent 继续推进。 整个证明过程，变成了一张被算力自动向前推进的拓扑网。 过去几百年，数学突破靠的是大师在黑板前的孤军奋战，靠的是漫长而脆弱的同行评审。 现在的数学验证，被拆成了绝对确定性的微内核与高并发的流水线。 技术的质变不在于 AI 学会了像数学家一样产生直觉。 它在于人类用严格的规则搭好了只允许真理通过的过滤器，然后把算力的闸门彻底拉开了。