11 天，1300 万行代码，AI 把数学界最著名的费马大定理从头到尾形式化了一遍

11 天，1300 万行代码，AI 把数学界最著名的费马大定理从头到尾形式化了一遍。 很多人第一反应是：AI 难道解出了人类解不开的难题？ 他们全看错了方向。 费马大定理早在 1995 年就被数学家安德鲁·怀尔斯（Andrew Wiles）彻底证明了。 Anthropic 的 Claude 既没有发明新理论，也没有发现新定理。 那为什么 Nat McAleese 和整个计算机科学界会把它视为分水岭？ 因为它打穿的不是数学创新的天花板。 是人类用了三百年的同行评议信任墙。 人类数学有一块谁都不愿意明说的软肋。 再顶尖的数学家，写出来的论文也充满了跳步： 「显然」、「同理可得」、「由对称性可知」。 只要论证逻辑大体通顺，几个同行审上几个月，盖个戳就算通过。 1993 年怀尔斯第一次公开证明时，六位顶尖审稿人整整查了一年，才在深处找出一个致命漏洞，逼得怀尔斯又闭关一年找来理查德·泰勒（Richard Taylor）才补齐。 如果是 500 页的望月新一 ABC 猜想呢？ 整个数学界看十年都没人敢给最终定论，因为没人有寿命逐行验算那几百页符号。 人类的大脑带宽，根本撑不起现代数学的验证复杂度。 为了彻底消灭漏洞，计算机科学家造出了 Lean 这样的形式化证明助手。 在 Lean 的世界里，不接受任何「显然」。 每一个定理都是一个严格的数据类型，每一次推理都是一段必须编译通过的代码。 从最基础的公理开始，每一个符号、每一个引理、每一个边界条件，全部要用形式化语言逐字敲出来。 只要有一行逻辑不严密，编译器立刻报错拒绝。 这就是确定性验证闭环。 一旦代码通过编译，数学真理就不再依赖任何学术权威的主观背书。 它是百分之百被机器焊死的绝对事实。 这套系统几乎完美，除了一点： 把人类的数学语言翻译成 Lean 代码，贵到了极点。 帝国理工学院的数学家 Kevin Buzzard 带领团队推进费马大定理的形式化工程，原本预计需要全球顶尖学者耗费五到十年的时间。 因为形式化代码格外繁重冗长。 人类数学家花十年建立的整个开源数学库 Mathlib，总共也就两百多万行代码。 谁愿意把最好的学术黄金期，花在给机器写逐行翻译上？ 形式化验证的门槛，被死死卡在了人类昂贵的时间成本上。 Anthropic 的解法，不是让单个模型去硬啃大部头。 研究员彭天翼（Tianyi Peng）团队搭建了 Prove2Me 协同系统。 他们把这套庞大的数学证明，拆解成一张包含近三万个子引理的有向无环图。 多智能体协同分工，各自负责攻克不同的引理节点。 每次 AI 写出一串代码，Lean 编译器就在毫秒级给出确定性反馈。 编译失败，AI 拿到报错立刻修正重写； 编译成功，这个引理就永久固化成整座大厦的一块基石，供给其他智能体调用。 大模型平时最让人头疼的幻觉，在这里被完全免疫。 因为编译器就是毫无妥协的铁面门卫。 大模型提供无穷无尽的探索直觉与代码生成力，形式化编译器提供零容忍的真理把关。 11 天时间，消耗 60 亿输出字符，生成 29511 个机器验证的引理，总代码量超过 1300 万行。 这是人类十几年积累的 Mathlib 体积的五倍以上。 这台机器的名字，叫形式化验证的边际成本崩塌。 它让知识的验证成本，从几百个顶尖学者的人年，直接降成了一次 GPU 集群的电费账单。 当这种机械级确定性的生产成本趋近于零，被重塑的远远不止纯数学。 航空航天的飞控系统、万亿美元级别的智能合约、最底层的芯片硬件逻辑、军用密码学协议； 所有过去因为「验证太贵、太难」而不得不默许漏洞存在的关键系统，第一次有了被全面形式化验证的可能。 人类不再需要通过漫长的辩论、声誉和权威去博弈信任。 只要给出公理，编译器就会给出判决。 过去我们以为 AI 会先学会像人一样天马行空地思考。 但这场突破表明，它正在成为一台不知疲倦的严密织网机，把人类散落了几百年的模糊知识，一针一线缝进绝对确定的机器逻辑里。