耗费人类顶级数学家八年隐居苦战的证明，被一群 AI 在 11 天里重构成了 1300 万行代码

耗费人类顶级数学家八年隐居苦战的证明，被一群 AI 在 11 天里重构成了 1300 万行代码。 这不是 AI 独立发现了什么新的数学大厦。 它完成的，是一场人类肉身几乎无法承受的公理级拆解。 1993 年，安德鲁·怀尔斯在剑桥大学宣布攻克了困扰人类 358 年的费马大定理。 全世界数学界为之沸腾。 几个月后的同行评审里，审稿专家却在第三章发现了一个致命的逻辑断裂。 那个断裂险些毁掉整个证明。 怀尔斯在崩溃边缘拉上理查德·泰勒，闭门补救了整整一年多，才在 1995 年正式修补完工。 为什么人类最顶尖的数学大脑，会把致命漏洞藏在眼皮底下？ 因为人类写数学论文用的是自然语言。 哪怕是划时代的殿堂级论文，通篇也充满了「显而易见」「容易推导」「按标准方法可知」。 人类的大脑工作记忆有限，根本装不下成千上万步底层的公理推演。 现代数学大厦的运转，依赖学者之间的同行信任与认知跳跃。 但计算机不认任何「显而易见」。 2024 年，帝国理工学院的凯文·巴扎德在数学界发起了一项庞大计划。 他组织全球学者，试图把怀尔斯的证明逐行翻译进计算机语言 Lean 4。 目标只有一个：把整个宏大论证拆解到不可再分的 3 个基本公理，消除所有人为疏漏的可能。 数学界原本预计，这项纯手工的翻译工程至少要耗费人类专家 5 到 10 年。 因为在形式化证明的世界里，把一页高等代数几何翻译成机器代码，往往需要专业学者苦敲数周。 然后，Anthropic 的 Claude 智能体集群接入了这场重构。 它们只用了 11 天。 产出了超过 1300 万行 Lean 4 代码，完整证明了 29,511 个中间引理。 独立的 Rust 验证内核 nanoda 审查了全部代码，没有任何一处报错。 为什么人类耗时数年的逻辑苦工，会被机器在几天内彻底荡平？ 这底下的核心机制，叫自动形式化。 过去大语言模型写数学，经常一本正经地给出幻觉。 但一旦把它接入形式化验证系统，游戏规则就彻底变了。 在 Lean 4 这种严格的类型系统里，一段代码要么逻辑严密通过编译，要么直接报错退回。 严密的编译器，成了绝对公正的真理裁判。 配合 Prove2Me 平台建立的有向无环图，成百上千个智能体在庞大的定理依赖树上同时开工。 每一个被攻克的引理，都会立刻固化成一块无法动摇的逻辑基石。 智能体不需要凭空构思灵感，它们只需要在形式化内核的实时反馈下，以极高的并发度扫清所有公理推演。 数学研究的分工，正在被这场试验永久重塑。 人类负责提出猜想、构想宏大的理论架构、搭建不同数学分支之间的灵感桥梁。 机器负责吞下数千万行枯燥、繁重、需要绝对严密的公理级对账。 科学的边界，从来不只受限于人类能构想出多么精妙的思想。 它同样受限于人类能有多大精力，去保证这些思想底下的每一块砖头都毫无裂痕。 当人类不再需要把毕生心力耗在繁复的公理对账上，真正深邃的数学探索，才刚拿到最锋利的放大镜。