11天1300万行代码，Claude碾平了折磨数学界350年的最著名证明：费马大定理被AI”形式化”了

11天1300万行代码，Claude碾平了折磨数学界350年的最著名证明：费马大定理被AI”形式化”了

如果过去三天你没看新闻，那你错过了可能是 2026 年 AI 数学史上最密集的核弹投放：

– 9月4日：GPT-6 Astra 发布，操作电脑、挖 0day、5道 Erdős 难题 – 9月5日：GPT-6 Astra 孪生素数上界推到 186 – 9月5日同一天：FME 基准发布，Astra 全场唯一非零分 – 然后今天凌晨：Claude 首发费马大定理形式化证明

Anthropic 宣布，Claude 在 11 天的连续运行后，完成了对费马大定理（Fermat’s Last Theorem）的首个端到端、计算机可验证的完整形式化证明。

费马大定理。1637 年费马在书页边写下”我发现了一个绝妙的证明，但这里空白太小写不下”。直到 357 年后，1995 年安德鲁·怀尔斯才用 129 页天书级的论文攻破了它。

今天，Claude 用 60 亿 Token、1300 万行 Lean 代码、30300 条可验证定理（29500 条被采用），以机器验证的方式重新走通了这个证明。

控制台弹出”PROVED”的时候，连 Claude 自己的内部日志都炸了——”.json! 费马大定理根节点读取为 PROVED……这是本次战役的目标……历史性的时刻。”

—

这不是 AI 自己想出来的证明——但这比”想出来”还吓人

先划重点。

Claude 没有发现一个新的、更简洁的费马大定理证明。 它做的是将怀尔斯 1995 年已有证明的简化版本（Darmon、Diamond、Taylor 版本）翻译成 Lean 证明助手可以逐行验证的形式化代码。

所以它不是”重新证明了费马大定理”，而是”把人类已有的证明，变成了机器可以逐条核对的形式化验证文件”。

但为什么我说这比”想出来”还吓人？

因为数学形式化这件事的难度，和”证明”不在同一个量级上——它是另一个维度的硬。

人类写数学证明的时候，有大量的”这里显然””不难看出””由引理3.2可得”。这些跳跃在人类读者那里是常识，但在 Lean 编译器面前，差一个引理都不行。你需要把整个证明链条上每一个省略的环节、每一个”显然”背后的前驱定理，全部展开到最底层公理。

帝国理工的 Kevin Buzzard 教授（数字界最坚定的形式化推动者之一）曾经牵头搞费马大定理的形式化，光是第一阶段蓝图就有 86 页，按他的估计——以年为单位。

人类预计要干好几年的活，Claude 干了 11 天。而且它是”基本自主工作”的。

多智能体 DAG 拓扑 + 姚班帅哥带队：英伟达黄仁勋等了一个下午

这场战役不是单个 Claude 模型单线程干的。

项目由清华姚班出身的哥伦比亚大学助理教授 彭天翼 发起。他的履历是标准的”开挂”: 清华姚班（2017 本科）→ MIT 运筹学博士（2023，GPA 5.0满分毕业）→ 哥大助理教授 + Anthropic 研究员。

团队使用的是一个叫 Prove2Me 的平台，核心结构是一张有向无环图（DAG）。每个节点是一个待证明的子定理，边是它们之间的依赖关系。几十个 Claude 智能体在这个 DAG 上并行工作：有些负责定义概念，有些证明中间定理，有些在验证其他智能体产出的证明逻辑。

人类研究员（主要是彭天翼）给出的”高层指令”大概是这种画风：”雅可比簇作为一个概形优先级挺高””尽快推进马祖尔定理”。

几个特别有意思的细节：

– 整个证明中，人类语言的注入量极低——几乎全是”这个定理先证明”这样的一句话指令； – Claude 从 Lean 编译器返回的错误中自主修正证明逻辑——它不需要人类来解释为什么编译报错； – Kevin Buzzard 审阅后认为”AI 辅助形式化大型数学已经取得重要进展”。

英伟达黄仁勋此前在 GPT-6 发布时连发两推，说”今天见证历史了”。然后 Claude 这个结果出来后，他下午的日程安排被改成了”看看 Claude 的费马大定理”——因为那天早上他还在夸 OpenAI。

AI 数学竞赛从”谁更聪明”变成”谁更卷”的速度，比所有人预期的都快。

1300 万行代码意味着什么？比 Mathlib 大 5 倍

一个直观的对比：Lean 的官方数学证明库 Mathlib，是人类数学家花了超过十年、成千上万的贡献者攒出来的全球最大的形式化数学知识库。

Claude 用 11 天产出的形式化证明规模，超过 Mathlib 的 5 倍。

而且它不只是为费马大定理本身写的。因为要从最底层开始搭，Claude 顺手证明了大约 2.9 万条中间定理——这些横跨代数、几何、数论、调和分析的定理，很多在此前根本没被形式化过。Claude 相当于以一场战役的姿态，打穿了整个现代代数数论的形式化版图。

Anthropic 已经把完整证明开源在 GitHub 上。所以如果你懂 Lean，现在就可以去下载 1300 万行代码，然后对着它们挠头说”这是什么”。

结语：数学的墙已经倒了

过去一周，整个数学界被 AI 敲了三下门：

第一天：GPT-6 Astra 开始做数学——孪生素数； 第二天：Astra 参加 FME 考试——全场唯一非零分； 第三天：Claude 交出了费马大定理的形式化证明——这是人类数学史上最著名的困难问题的完整机器验证形式化。

形式化和证明之间的关系，有点像”翻译原文”和”写原著”的区别。但这次翻译的原文厚度与复杂度，已经远远超出了人类可独立管理的范围。

从 7 个月 (清华 FormaTheoria)、到 11 天 (Claude 费马大定理)、到实时逼近 (Astra FME)。AI 形式化的速度从”以年为单位”，正在向”以天为单位”加速。

彭天翼干了一件足以写入 AI 历史的事。Anthropic 干了一件让 OpenAI 没法喘气的事。数学界干了一件从今往后再也不能假装”AI 只是在做奥数题”的事。

那扇门打开了。里面是 Lean 编译器的绿色 “PROVED”。

外面是 350 年的墙，已经倒了。