费马大定理有了第一个机器可验证的证明：Claude 用 11 天写了 1300 万行 Lean

原文来源：Anthropic — Anthropic 分享费马大定理第一个完整的机器可验证证明：Claude 用 11 天、1300 万行 Lean 代码完成。

费马大定理，曾是最著名的数学猜想之一，如今有了第一个机器可验证的证明。Anthropic 在 9 月 4 日公布了这项成果：Claude 近乎自主地工作了 11 天，用 Lean 证明助手写完了这个证明——这是人类第一次把整个证明完整地交给机器检查。

先说清楚这次突破的边界：它没有产生新数学——费马大定理早在 1995 年就被安德鲁·怀尔斯证明了。它改变的是验证这件事本身。过去审阅一个重大数学证明需要数月甚至数年，如今机器可以在逻辑层面逐行确认。Anthropic 自己也点出这个区别：最近用 AI 研究黎曼假设的工作产出的是新数学，而这次的新意在于验证——把证明像计算结果一样交给机器核对。

11 天、1300 万行、29,500 个中间定理

费马在 1637 年把猜想写在了《算术》一书的页边空白处：不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ（n > 2）。此后三百多年，无数数学家尝试证明。1908 年有人悬赏 10 万德国金马克（约合今天一两百万美元），悬赏第一年就收到了 621 份错误证明。

怀尔斯 1995 年的证明有 129 页，验证过程本身就花了几个月——1993 年他首次公开宣布证明后，一位审阅者的问题暴露了证明中的关键缺口，怀尔斯花了一年才补上。证明之复杂，让"形式化"（把数学推理转换成计算机能自动检查的形式）成了此后几十年的工程难题。2024 年，帝国理工的 Kevin Buzzard 发起了一个社区项目，打算用 Lean 完成费马大定理的形式化，仅项目蓝图就有 86 页，社区预期要花数年。

这次 Claude 的成果是：11 天完成。过程数据相当惊人：

• 最终证明 1300 万行 Lean 代码，是 Mathlib（Lean 社区的数学定理库，整个证明都以它为基础）的 5 倍以上
• 过程中产出了 30,300 个定理的机器可验证证明，其中 29,500 个被最终证明采用
• 数十个 Claude agent 协作分工：定义概念、证明中间定理、逐层攻克更难的问题
• 总消耗约 60 亿输出 token，用的是 Anthropic 内部研究模型（大致相当于 Claude Fable 5.1 的水平）
• 人工输入极少：Anthropic 研究员 Tianyi Peng 只偶尔给出高层指令，比如"优先处理 Jacobian 这类概形（scheme）"

项目并非一帆风顺。文章披露，早期尝试中多个 agent 协作很快失效——它们会弄丢项目状态、停止有效配合。最终成功靠的是切换到 Prove2Me——一个由 Tianyi Peng 与哥伦比亚大学团队设计的开放数学形式化协作平台。失败的早期尝试贡献了最终证明中约 7% 的非样板代码行。

最终验证干净利落：证明只用了 Lean 的三个标准公理，一个比对工具确认了定理陈述与 Mathlib 中费马大定理的陈述完全一致。Kevin Buzzard 本人审阅了这个证明，认为这是"非凡的自动形式化成就"。

为什么这件事比"AI 会做数学题"重要得多

对普通读者来说，"AI 证明费马大定理"听起来像又一个 AI 炫技新闻。但真正值得关注的，是它把数学界的评审机制往前推了一大步。

数学知识建立在一个脆弱的信任链条上：一个新证明是否正确，靠的是少数专家经年累月的审读。如果链条里有一环是错的，后续建立在它之上的所有工作都可能崩塌。而 AI 正在以前所未有的速度产出证明——人类审稿人根本跟不上。Anthropic 的观点是：形式化证明会成为常态，任何写给人类读者看的工作都会附带一份机器可验证的版本。"虽然我们不认为形式化证明应该取代人类可理解的论述，但这可能是数学界跟上 AI 产出速度的唯一可行方式。"

还有个有趣的附带发现：写 Lean 似乎也在帮助 Claude 证明新结果。Anthropic 最近的多个成果都是证明与形式化同步进行的——Claude 会像研究者写数值模拟验证思路那样，先用部分证明独立检验自己的假设。

成本也没有想象中那么遥不可及。文章记录了一个小实验：用三个个人版 Claude Max 订阅，通过 Prove2Me 协作，agent 团队 3 天就完成了 Vinogradov 三素数定理的形式化——这说明用消费级 AI 订阅协作形式化重大定理是可行的。

独立的视角：机器验证不等于人类理解

这项成果确实令人兴奋，但也值得冷静地看几点。

第一，"可验证"和"可理解"是两回事。 1300 万行 Lean 代码是 Mathlib 的 5 倍——这个规模远超任何人类能通读的范围。Buzzard 的背书和 Lean 的逐行检查证明了证明的正确性，但人类数学界要"理解"这个证明（从中学习、在其上构建），面对的是一个比怀尔斯那 129 页的书面证明大得多的庞然大物。正确性有保证，可读性没有。

第二，成本门槛依然存在。 60 亿 token 的内部模型消耗不是普通研究者能轻松复现的。消费级实验（3 个订阅 3 天证三素数定理）给了希望，但"三素数定理"和"费马大定理"的复杂度差距，恰如蓝图里那 86 页与 1300 万行的差距。

第三，agent 协作仍是这套流程里最脆弱的一环。 早期尝试中 agent 集体失联、项目状态丢失——这种失败模式在软件工程里似曾相识。11 天的成功建立在 Prove2Me 这个外部脚手架之上，如果面对一个没有这类基础设施的问题，agent 团队能维持多久的稳定协作，仍是未知数。

完整证明已开源在 GitHub 上，附有一份分步讲解（walk-through）。对数学界来说，这或许正是一个分水岭：验证的成本在急剧下降，而人类需要适应的，是学会信任一台机器逐行确认过的、自己却读不完的证明。

数学正在进入一个微妙的阶段——AI 负责产出和验证，人类负责理解和判断方向。费马大定理只是第一个完整走完这套流程的案例，接下来的问题是：当验证变得廉价，数学研究的重心会向哪里迁移？