就在今天凌晨，Anthropic 公布了一份费马大定理的完整机器校验证明：Claude 大体自主工作了 11 天，写出约 1300 万行 Lean 代码。
发起这项实验的是彭天翼（Tianyi Peng），Anthropic 研究员、哥伦比亚大学助理教授，也是清华姚班校友。他最初想试试 Claude 能把这项形式化工程向前推进多远，最后收到了一个完整结果。
这个实验使用的是 Claude 内部通用研究模型。Anthropic 对它的描述是，能力大致相当于 Claude Fable 5.1。
费马大定理早已有 Wiles 的数学证明。Claude 这次沿着既有证明路线，把大量推导补成了计算机能够逐步检查的形式。
1300 万行代码背后，既有数学家的积累，也有一群 Agent 如何把庞大任务做到底的问题。
论文里的“显然”，计算机也要查
费马大定理的命题很短：当整数 n 大于 2 时，不存在正整数 a、b、c，让 aⁿ + bⁿ = cⁿ 成立。
但一句话能说完的命题，证明起来可以极其复杂。Wiles 的证明要用到许多已经建立的数学结果，Claude 此次参考的就是 Darmon、Diamond 和 Taylor 对这条路线的阐述。
数学论文是写给同行看的。作者可以省略读者熟悉的推导，引用已有定理，把一段过程压缩成一句“由此可得”。
到了 Lean 这样的证明助手里，省略掉的依据就得接上：每一步用了什么前提，引用了哪条结论，结论又依赖什么，都要写成检查器可以核对的形式。
所以，形式化一份复杂证明，往往需要先形式化它下面的一大批数学基础。Claude 的工作建立在 Lean、Mathlib，以及 Kevin Buzzard 团队的 FLT 项目等人类开源成果之上，再继续补齐所需的定义和证明。
彭天翼对长证明难以核验这件事，有过切身经历。
Anthropic 的文章讲到，他本科时，导师曾希望把他论文中的成果写进一篇《Nature》文章。导师问他，能不能确认证明正确。
他给出的回答是，自己有 99% 的把握，但这么长的证明，很难百分之百确信。最终，这次发表机会与他擦肩而过。
这个细节也让“机器校验”有了很具体的意义：当一份证明长到难以逐步审完时，研究者需要一种能继续追查推理依据的工具。
多个 Agent，也会跟丢项目进度
把 Claude 叫来之后，实验并没有一路顺利。
Anthropic 披露，早期 Agent 虽然取得了一些进展，却很快跟不上项目的整体状态，难以继续有效协作。
一个中间定理已经证明了吗？它还缺哪些前提？另一个 Agent 做出的结果，自己能不能接着用？
任务越大，这些问题就越难靠一段对话的上下文记住。会做眼前的题，还得知道眼前这道题在整个工程里的位置。
转折点是 Prove2Me，彭天翼及其哥伦比亚大学合作者为数学形式化开发的协作平台。
它先把定理之间的依赖关系组织成一张 DAG。每个节点对应一个定理陈述，连线说明它依赖哪些前面的结果。Agent 据此决定下一步尝试什么证明，多个 Agent 也能围绕这张共同的进度图并行工作。
平台还把定理陈述和具体证明分放在不同文件中，单独维护它们之间的关系。这样能加快 Lean 编译。
每个定理又配有自然语言描述，方便 Agent 搜索和复用。已经完成的工作因此更容易被找到，后续证明可以站在这些结果上继续往前走。
Prove2Me 配合基于 Claude Code 的多 Agent 框架，让局部结果逐渐汇入同一份完整证明。定义概念、证明中间定理、利用已有定理继续推导，这些工作终于能接续起来。
据 Anthropic 介绍，整个任务消耗了约 60 亿个输出 token。11 天的背后，是大量计算，以及让这些计算持续朝同一个目标前进的协作安排。
这一段对做 Agent 的人尤其熟悉：除了把单次推理做强，还得把进度、依赖和已完成结果放到后续任务能够查到、用上的地方。
1300 万行，怎么确认它真的成立
证明生成出来之后，验收交给了另一套程序。
Lean 内核负责检查推理。仓库报告显示，这份证明只依赖 Lean 的三项标准公理，整个证明可以通过内核重放检查。
还有一道容易被忽略的检查：它证明的命题，得确实是我们要的费马大定理。
仓库使用 comparator，把最终命题与 Mathlib 中的标准表述进行比较，确认最终命题一致。这样检查的是同一个目标，不能悄悄换成一个更容易成立的版本。
这让“写出证明”和“检查证明”各自有了明确的工作。Claude 生成推导，协作平台组织这些推导，检查器再核对它们能否从规定的前提出发，得到目标结论。
外部数学家也实际检查了这份成果。
长期推动费马大定理形式化的 Kevin Buzzard 在自己的博客里说，他编译了代码库，并运行 comparator，检查通过。
有意思的是，他最初收到邮件时，根本没把这件事当真。
当时 Buzzard 正在参加音乐节。他看到一封关于费马大定理完整形式化证明的邮件，一度以为是民科来信。
一周后，他清理积压的未读邮件，才认真了解到这项成果。后来，曾经被他略过的邮件，变成了一份他亲自编译检查过的证明。
最后还有一个很小、却很熟悉的插曲。
Ethan Mollick 转发消息时，注意到了仓库 README 的简介。他调侃，费马大定理证明的介绍这么短，仍然有很明显的 Claude 文风，尤其是“为每一步命名，并标出支撑它的 Lean 定理”这样的写法。
参考链接
Anthropic 研究原文：https://www.anthropic.com/research/formalizing-fermats-last-theorem 彭天翼本人学术主页：https://tianyipeng.github.io/ 费马大定理 Lean 4 证明仓库：https://github.com/anthropics/fermats-last-theorem Kevin Buzzard 本人记录：https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ Ethan Mollick 原帖：https://x.com/emollick/status/2095957821644763561