Claude 仅用 11 天便证明了费马大定理——接下来会发生什么？

11天里见证不可能

费马大定理是数学界最古老的未解问题之一。17世纪，皮埃尔·德·费马在一本书的页边空白处随手写下一条猜想：不存在三个正整数 a、b、c，使得 a^n + b^n = c^n 对任何大于 2 的整数 n 成立。这个问题在三百多年间拒斥了所有尝试，直到1995年安德鲁·怀尔斯发表了一篇证明——长达129页、论证高度密集的论文，令整个数学界耗时数月才完成全面验证。

如今，Claude 用 11 天就给出了该证明的机器可检验形式化版本。

数字令人咋舌：约 1300 万行 Lean 代码。在整个过程中证明了约 33,000 条独立定理，其中约 29,500 条被用在最终输出里。该证明只依赖 Lean 的三个标准公理，且没有出现一个 sorry 占位符 —— 即那些通常标志“形式化证明仍在依赖人类信任而非机械验证”的不完整断言。

帝国理工学院一支由 Kevin Buzzard 领导的团队早在 2024 年就开始了同样的形式化项目。仅他们的初步规划文档就达 86 页，预计耗时数年。

Claude 究竟是如何做到的

Anthropic 研究员 Tianyi Peng 让 Claude 着手解决这一问题，并在项目中部署了数十个 Claude Agent。每个 Agent 负责不同模块——从定义、中间引理开始，逐步攻克更难的核心命题。整个系统自底向上构建证明，如同搭建一座大教堂，一块石头一块石头垒起。

但真正的挑战在于协调。早期的尝试失败，是因为每个 Agent 都丢失了对整体项目状态的追踪，无法复用彼此的工作成果——多 Agent 系统并不会自动扩展到以年为单位的漫长工程中。

Peng 及其团队用 Prove2Me 解决了这一问题。这是一个专为数学形式化打造的协作平台：它以有向无环图（DAG）管理定理间的依赖关系，让多个 Claude Agent 始终清楚哪些结果已就绪、哪些定理仍需攻克。该平台将定理陈述与证明分离到不同文件中以加速编译，并为每条结果附上自然语言解释，便于搜索与复用。

最终结果通过了 Lean 的标准内核校验。它也在 nanoda 中通过了验证——这是一个用 Rust 独立实现的 Lean 内核，在一百万余条声明的检验中未报任何错误。一项对比工具还确认，该证明的目标与 Mathlib 现有的（尚不完整的）费马大定理编码指向同一命题。

这绝不只是数学戏法

其意义远超纯数学，背后有更深层的原因。

Lean、Coq、Isabelle——这些定理证明器不只是校验数学。它们校验任何可表达为形式化逻辑系统的内容。验证数论证明的基础设施，同样可以验证微内核、分布式协议、密码学库。

理论上，软件形式化验证早已可行。但在实践中，代价高昂得令人却步。把哪怕中等规模的软件代码翻译为形式化逻辑所需的工作量，增长速度远超任何组织的预算承受能力。正因如此，大量关键基础设施——TLS 库、操作系统内核、飞行控制系统——仍运行在从未有人做过形式化正确性证明的代码之上。

Claude 对费马大定理的形式化，展现出与以往 AI 辅助定理证明截然不同的质变。早期工作，包括 Google DeepMind 的 Gato 和 Meta 的 LeanCoPT，仅在更小、更短的问题或序列上产出证明。关键区别在于规模与完整性：这不是玩具问题，而是现代数学中最深刻的成果之一；其形式化版本完整、自洽，并经独立验证。

实际后果：验证从不可行走向可负担

如果一个 AI 系统能在 11 天内产出一条完全可验证的形式化证明——而该证明由人类数学家耗费数十年构建、再耗费数年才能形式化——那么同一条流水线便可同样应用于软件。

以 nanoda 所在的 Rust 生态为例。Rust 已有坚固的内存安全保证，但这些保证仅针对单个程序，而不覆盖整个依赖链。一条经形式化的证明库意味着：你可以自底向上、精确到比特层面地验证自己的密码例程确实实现了你以为它实现的那个算法。

瓶颈也随之转移。瓶颈不再是写出形式化证明本身，而是写出规范（specification）——你到底要证明什么？这个问题仍然极其人性化。但填补缝隙、串联引理、处理边界情况这些机械性劳动，现已可委托给机器。

基准测试的意义

每个主流 AI 实验室都将定理证明视作一种“可信度信号”。通过普特南考试、解答 IMO 题目、产出 Lean 证明——这些基准之所以重要，是因为在一个几乎无法隐藏幻觉（hallucination）的领域里，它们是检验通用智能的试金石。证明若不通过，就是不通过，绝无侥幸过关的可能。

Claude 的费马大定理形式化显著拉高了门槛。此前基准衡量的是更小、经过筛选的问题上的进步；而这是一次从零开始、完整、自洽地形式化一项里程碑式成果的尝试，零漏洞且经独立内核验证。这使得未来任何此类基准若不能触及同等深度的问题，都将显得微不足道。

当然，也有一处警示：该证明大量依赖 Mathlib——即已有的 Lean 数学库。1300 万行代码中，相当部分是基础设施与已知结果的重形式化，而非全新的数学洞见。真正的问题在于：Claude 能否更进一步——即在没有任何已有编码表示的情况下，仍能产出全新结果的形式化，而不仅是在现有基础上的延伸。

谁赢谁输

Anthropic 赢得了这场可信度竞赛。费马成果为他们带来了一项具体、无可争议的成绩，无人能以“刷榜”轻易 dismiss。同时，这也印证了他们多 Agent 架构与 Prove2Me 平台是严肃工具，而非仅作研究演示的玩具。

人类形式化团队则失去了一些紧迫感。Buzzard 在帝国理工的项目早已启动，而 Claude 仅用一小段时间就完成了原本数年才能完成的成果。这并不意味人类主导的形式化工作就此失去意义——在研究层面，人类数学家对这些证明背后的结构与直觉的理解依然无可替代——但它确实意味着：在“把已有知识编码进机器”这一赛道上，人类正逐渐被 AI 主导。

若 Software 行业足够留意，则是赢家。我们能证明的代码与我们实际部署的代码之间的鸿沟，长久以来是计算领域最昂贵的低效之一。AI 若能将哪怕一小部分鸿沟填补上，从医疗设备到金融系统的一切可靠性都将大幅提升。

AGI 怀疑论者则失去了一项有力论据。形式化定理证明长期被视为 AI 难以达到人类等效水平的典型领域；而 Claude 在此项基准上的超越幅度，已相当于此前被认为“至少还需数年”的进展。这是否构成 AGI 另当别论——但它无疑展示了一项在 2024 年之前无法被合理预见的的能力跃迁。

接下来会发生什么

Anthropic 在原材料中表达的预期是：机器可检验的形式化证明将与人类可读的论文并行成为标准。这算是保守预测；更可能的演化路径会更快。

紧接而来的，是把 Prove2Me 应用于其他里程碑定理——素数定理、四色定理、开普勒猜想。每一项各有形式化难点，但流水线已经跑通。问题不再是“是否可行”，而是 Claude 能在触及架构极限之前处理多深的理论。

随后便是软件。若同样的多 Agent 框架能形式化一份 129 页的数论证明，那么它同样能形式化 TLS 实现、分布式共识协议、编译器前端。规范更难写——软件行为不同于抽象代数——但核心问题相同：弥合非形式化断言与机械可验结果之间的鸿沟。

那 1300 万行代码并非故事的全部。真正的故事在于：瓶颈已经移动。

GitHub 仓库：https://github.com/anthropics/fermats-last-theorem