1300 万行代码，29511 个定理，只为了验证 30 年前一个早就被人类承认的数学结论。 很多人以为这是 AI 又在…

1300 万行代码，29511 个定理，只为了验证 30 年前一个早就被人类承认的数学结论。 很多人以为这是 AI 又在抢数学家的饭碗。 全看反了。 AI 没有提出任何新公式，也没有发现任何新定理。 它干的，是一场对人类知识库的终极验资。 1995 年，安德鲁·怀尔斯（Andrew Wiles）发表了费马大定理的完整证明。 130 页的天书，浓缩了数论三百年来的顶峰。 当年全世界能彻底读懂那份手稿的学者，一只手就能数得过来。 为了挑出里面的漏洞，数学界最顶尖的同行评议团队关门审了几个月。 后来甚至真发现了一个致命断点，怀尔斯又拉上理查·泰勒（Richard Taylor）闭关整整一年才打上补丁。 这暴露了现代科学体系里一个没人愿意承认的隐形危机： 当人类最前沿的知识变得越来越庞大、逻辑链条越来越漫长，我们凭什么确定那些所谓的权威证明里，没有藏着下一个谁也没发现的断裂点？ 这台长期卡死科学前沿的冰冷机器，叫作形式化编译。 人类数学论文是用自然语言写的。 字里行间写满了「显而易见」、「同理可得」、「读者自证不难」。 这种交流靠的是同行之间的智力直觉和信任。 但计算机不讲信任。 在 Lean 4 这类交互式定理证明器里，没有模糊空间。 每一个数学定义，都必须从最底层的 3 个基本公理出发，一步一步推导。 中间只要漏掉一个逻辑断点，整个程序直接报错。 把人类顶尖论文逐字逐句翻译成这种防弹代码的过程，就是形式化编译。 帝国理工学院的数学教授凯文·巴扎德（Kevin Buzzard）此前领衔了费马大定理的人类形式化工程。 那是全球几十位顶尖数学家组成的协作团队。 他们的预期时间表，是手工啃上五到十年。 因为要把 1995 年达蒙-戴蒙德-泰勒（Darmon–Diamond–Taylor）的那套论述体系全部拆碎、转译成代码，是一场极其耗费心智、容错率为零的高精度苦工。 人脑的验证带宽，在这里被推到了物理极限。 哥伦比亚大学彭天翼团队开发了 Prove2Me 协作框架，让多个 Claude 智能体共享一个有向无环图，把整个证明任务拆解成数万个逻辑节点并发推进。 11 天。 1300 万行 Lean 4 代码。 29511 个中间引理。 最终通过了独立的 Rust 内核验证器 nanoda 检验，没有留下一处未经证明的空缺。 荷兰数学家维迪克（Freek Wiedijk）在二十多年前列出的百大数学定理形式化清单，在这一刻被画上了最后一个勾。 这件事情的分水岭，不是 AI 拥有了人类的数学灵感。 是科学知识的信任机制，第一次拥有了工业级的自动化验资机。 过去几百年，人类积累知识靠的是同行评议与权威背书。 论文发在顶级期刊，几位审稿人点头，整座学术大厦就建在这份共识之上。 但当现代科学的深度远远超出人类肉眼的核查速度，信任就变成了最昂贵的风险。 当形式化编译被这套系统跑通，数学、密码学、芯片架构与底层软件的逻辑链条，第一次可以在几天内完成全量穷尽式的硬核校验。 这场突破的核心价值，不在于机器替人省下了多少算力。 在于它把那道横亘在人类文明头顶几十年的信任成本，一次性压到了零。