13 百万行 Lean、29,511 个定理：Claude 如何把费马大定理形式化 (2026)

费马大定理本身由安德鲁·怀尔斯在 1995 年证明。Anthropic 于 2026 年 9 月 4 日发布的结果，完成的是把这条现代证明路线写成 Lean 代码，再交给证明助手逐步检查；Anthropic 将它称为首个端到端、机器校验的费马大定理形式化证明。1

这项工作的关键成果不是一个模型独自“想出了”新的数学，而是一套多智能体工程把数千页数学论证拆成共享依赖图中的数万个命题。最终工件有约 1300 万行 Lean，最终定理的依赖树包含 29,511 个定理；运行过程中累计证明的定理约为 30,300 个。2 3

先把“证明”说准：新增的是形式化

费马大定理断言：对于大于 2 的整数 n，不存在正整数 a、b、c，使 a^n + b^n = c^n。怀尔斯的证明已经解决了这个数学命题。Anthropic 这次处理的是另一项工作：把人类读得懂的数学论证，改写成 Lean 能逐项检查的定义、命题和证明项。

人类证明会省略“显然”的代数变形，也会直接调用书本和论文中的结果。Lean 要求这些步骤都出现在形式系统里，而且每个外部结果也要有对应的形式化版本。Anthropic 的官方说明说，费马大定理的形式化原本预计需要多年；仅 Imperial College London 项目用于描述初始阶段的 blueprint 就有 86 页。1

因此，机器校验首先保障的是一个精确的 Lean 命题：在指定的 Lean、Mathlib 和依赖文件下，证明项能够通过内核检查。这个保障很强，却和“模型独立发现了费马大定理的新证明”属于不同命题。Kevin Buzzard 在 Xena Project 的独立记录中也把这项工作描述为沿用既有证明路线的形式化，认为它对数学内容本身没有增加新的结果。4

11 天靠的是共享依赖图

Anthropic 最初让 Claude Agent 直接推进大型形式化项目时，Agent 很快丢失项目状态，协作也逐渐失效。切换到 Prove2Me 后，系统为每个待证命题维护依赖关系，多个 Agent 可以同时领取不同节点；一个节点完成后，后续节点就能把它作为输入。

Prove2Me 的作用集中在三个工程机制上：

DAG 保存定理依赖。 有向无环图把最终目标拆成层层相连的命题，Agent 可以根据未完成的子节点决定下一步工作，也能避开已经关闭的分支。
命题与证明分开存放。 系统把“要证明什么”和“怎样证明”放进不同文件，再独立维护两者的连接。这样做既减少 Lean 编译的资源消耗，也让一个证明失败时不必重写整棵树。
自然语言描述支持检索和复用。 每个命题都有可搜索的文字说明，后来的 Agent 可以找到已有结果，而不是在不同文件中重复构造同一个中间定理。

Prove2Me 的公开论文把平台定义为一个开放协作的数学形式化系统：人类用户发起形式化任务，AI Agent 向共享任务贡献证明，平台用机器检查保证局部结果能够接入依赖图。5

费马大定理 Lean 证明的依赖路径图 — *Anthropic 官方图把证明路径分为 Mazur、Ribet 和 Wiles 三条支路，三条支路最后汇入费马大定理；框内同时列出对应的 Lean 命题名称。1*

这个过程的“11 天”是墙钟时间，不是单个模型连续写代码的时间。Anthropic 说，项目由数十个 Claude Agent 并行完成，使用一个大致相当于 Claude Fable 5.1 的内部通用研究模型，消耗约 60 亿输出 token。1 结果说明了模型、任务分解、共享状态和验证器的组合效果；单独拿“11 天”来衡量模型本体，会把这些因素混在一起。

数学路线沿用怀尔斯体系

证明依赖图不是把费马大定理改写成一条全新的数学路线。Anthropic 的 PDF 说明，项目采用 Henri Darmon、Fred Diamond 和 Richard Taylor 对怀尔斯及 Taylor–Wiles 论证的简化说明。

路线的功能关系可以压缩成一条链：一个费马大定理反例会导出一条 Frey 椭圆曲线；Mazur 的结果用于处理这条曲线的模 p 表示的不可约性；Langlands–Tunnell 定理和 3–5 切换为模性论证提供入口；Wiles 的模性提升步骤证明这条半稳定椭圆曲线具有模性；Ribet 的降层定理再把表示降到 2 级，那里不存在所需的权 2 尖点形式，于是反例不能存在。2

这条链说明了形式化的难点：项目需要把代数、调和分析、几何和数论中的深层结果，全部放到同一个可检查的依赖环境里。Agent 的工作单位因此不是“写一段长证明”，而是声明一个命题、核对它的假设、寻找依赖、生成 Lean 证明，再等待其他节点接入。

四层检查，各自回答不同问题

最终工件的可信度来自几层检查。每一层都解决不同的错误来源，读者不能把其中一层的通过结果替换成另一层的结论。

Prove2Me 逐卡检查。 平台会针对每个命题检查其证明是否成立，并根据子节点的声明继续向上合并。这个结果说明局部证明可以接在已声明的子命题上，但平台上的单卡“Proved”本身还不是整棵树的一次性构建。
完整 Lean 构建。 项目发布后，团队从源文件重新编译整个证明树。仓库的 FinalCheck.lean 会检查最终定理只依赖 Lean 的三个标准公理 propext、Classical.choice 和 Quot.sound，并排除 sorry、额外 axiom 和其他会绕过正常证明检查的构造。3
comparator 对齐命题。 comparator 把项目中的最终命题与 Mathlib 自己的费马大定理命题进行比较，确认两者涉及的声明和常量一致。这个步骤回答的是“代码证明的究竟是不是目标命题”，而不只是“代码证明了某个同名命题”。3
nanoda 独立内核。 nanoda 是用 Rust 编写的 Lean 内核独立实现。仓库记录的结果是，它检查了 1,052,234 个声明且没有报错；项目同时公开了用于加速检查的补丁，并说明这些补丁没有修改类型规则。3

这四层把“平台上的局部证明”“整棵树的 Lean 构建”“最终命题的对齐”和“另一套内核重放”分开了。它们共同支持的结论是：公开的 Lean 工件在给定环境中通过了机器检查。

机器检查之后还剩下什么

Lean 内核检查的是形式系统中的证明关系。它不会自动判断每个中间定理的名字是否准确表达了数学含义，也不会把机器生成的文件变成人类可以顺畅阅读的数学教材。Anthropic 的仓库明确提醒，名称和声明不一致时，以实际 Lean 声明为准；仓库的英文摘要和建议引用也有自动生成部分。3

公开工件还依赖此前的社区工作。仓库说明，106 个文件改编自 Kevin Buzzard 领导的 Imperial College London FLT 项目和 flt-regular 项目，同时建立在 Mathlib 之上。这个事实不会削弱最终命题的内核检查，却改变了“从零开始自动产生全部数学基础”这一说法的含义。3

可维护性也是另一条边界。仓库把成果标为 research artifact，注明项目目前不维护，也不接受贡献。Kevin Buzzard 的记录则指出，成品完成了比 Imperial 项目当前阶段更完整的端到端形式化，但他自己的项目还承担着把现代数论对象整理成适合人类探索、审阅和进入 Mathlib 的动态文档这一任务。3 4

复现成本决定它能否成为日常工具

Anthropic 的公开仓库给出的复现条件相当具体：需要 Linux 或 macOS、Lean 4.33.1、联网获取 Mathlib，以及足够大的内存和磁盘。仓库作者报告，在 96 个并行任务下，完整构建约需 5 小时 32 分钟，峰值内存约 153 GB；comparator 约需 14 小时 46 分钟，峰值内存约 230 GB；nanoda 的检查约需 30 分钟和约 40 GB 内存。3

这些数字把“可复现”分成了两层：任何人都可以下载源代码、查看依赖图和阅读构建脚本；完整重放则需要接近服务器级别的计算资源。对于研究团队，复现的第一步应当是锁定 Lean 工具链、Mathlib 版本和提交记录，再分别记录完整构建、命题对齐和独立内核检查的结果。

Anthropic 还给出了一个规模更小的实验：三个个人 Claude Max 计划通过 Prove2Me 协作，在三天内完成了 Vinogradov 三素数定理的形式化。这个实验说明脚手架有机会把形式化任务交给普通订阅账户完成，但它只有一个小样本，无法推出一般性的成本或成功率结论。1

这项工作的可靠判断可以落在一个较窄的位置：Claude 已经能够在共享依赖图和多层检查器的配合下，产出大型、可重新构建的数学形式化工件。接下来真正值得观察的是，类似系统能否同时提供人类可读的证明叙述、可复用的通用定理、清晰的上游归属，以及普通研究团队承担得起的复现路径。数学命题的正确性由内核检查，证明的语义、可维护性和研究价值仍需要人来判断。