AREX Feed Article
Anthropic 官宣：Claude 约 11 天完成费马大定理首个机器可验证证明
9 月 4 日，Anthropic 在官方 （文章题为《Formalizing Fermat's Last Theorem》）宣布，其模型 Claude 在约 11 天内基本自主地完成了费马大定理（Fermat's Last Theorem，FLT）的首个完整机器可验证证明：代码用交互式定理证明器 Lean 写成，超过 1300 万行，包含约 29,500 条中间定理，整个证明只用 Lean 的三个标准公理即可验证，无需任何额外假设。
完整代码已公开在 GitHub 仓库 （创建于 UTC 9 月 4 日 14:21，顶部贡献者一栏写着 claude）；@AnthropicAI 于 UTC 18:50 在 X 上发帖官宣，称这是迄今写下的最大 Lean 证明。主导人类 FLT 形式化项目的帝国理工学院（Imperial College London）Kevin Buzzard 已在记录了自己的复核：他亲自编译了整套代码并运行 comparator（证明比对器），结论是「它通过了（it checks out）」。
新意不在数学，在验证
故事要从 1637 年讲起：费马在《算术》书页空白处写下，他发现了一个「真正美妙的证明」，可惜「页边太窄写不下」。此后 350 多年无人找到这个证明；1908 年公开悬赏 10 万德国金马克征求正确证明，仅第一年就收到 621 份错误尝试。Anthropic 博客重述了这段历史：1993 年 6 月，Wiles 用三天讲座宣布证明，两个月后审稿人的一个提问暴露出关键缺口；他独自补救近一年、一度濒临放弃，最终与 Richard Taylor 一起在 1995 年 5 月发表正确证明——论文长 129 页，人类复核花了数月。
Anthropic 把这次工作与近期围绕黎曼假设的 AI 数学成果区别开：那批工作产出了新数学，而「这里的新东西是验证」——把一篇数学证明当作计算题交给机器核对。核对并不轻松：写给人类看的证明会跳过大量「显然」的步骤，Lean 却要求每一步都显式写出；人类证明可以引用几个世纪的文献积累，形式化只能从已被形式化的那一小部分数学重新搭起。仅描述项目第一阶段的人类蓝图就有 86 页，社区此前的预期是这项工作需要数年。
成果的体量因此超过既有积累：这份证明是 Lean 社区主数学库 Mathlib 的 5 倍以上；X 帖补充说，它覆盖了许多此前从未被形式化的数学领域。
Prove2Me：60 亿 token 与一张定理依赖图
这项尝试由 Anthropic 研究员 Tianyi Peng 发起（博客称他在哥伦比亚大学的小组专做 AI 形式化工具）。Anthropic 自述，最初的几次尝试并不顺利：智能体虽有早期进展，但很快丢失项目状态、协作失效；这些失败尝试的产出仍贡献了最终证明中约 7% 的非样板代码行。
转折点出现在切换到 Prove2Me——一个由 Tianyi Peng 与哥伦比亚大学合作者设计的开源协作形式化平台。博客列出它的三项作用：用定理陈述构成的有向无环图（DAG）帮智能体决定下一步证明什么，缓解记忆退化、支持多智能体并行；把定理陈述与证明分文件存放、独立维护关联，加快 Lean 编译、降低资源消耗；为每条定理保留自然语言描述，便于检索复用。配合一个基于 Claude Code 的多智能体框架，数十个 Claude 智能体分工定义概念、证明中间定理，再叠加出更难的结果。
博客还公布了 Claude 使用的 Prove2Me 计划关键里程碑图：
人类输入被压缩成偶尔的高层指示，例如「把 Jacobian 作为概型写出来，优先级很高」「尽快把 Mazur 定理做完」。
博客贴出的 Claude 思考日志摘录记录了收尾时刻：「FLT 根定理在网站上显示 Proved。历史性时刻（待复核）。」「FLT 根定理于 8 月 18 日 02:00:57（UTC）在 prove2me 上显示 PROVED。」整个流程消耗约 60 亿输出 token，所用模型是 Anthropic 内部一个通用研究模型，博客称其水平大致相当于 Claude Fable 5.1。
60,475 个模块如何通过三重核验
仓库 README 把「如何验证」写成可复现的流程。证明的最终陈述是定理 fermat_last_theorem：对所有正整数 a、b、c 与 n ≥ 3，aⁿ + bⁿ ≠ cⁿ。
默认构建目标 FinalCheck.lean 用 #guard_msgs 断言公理依赖列表，构建只有在证明恰好依赖 Lean 的三个标准公理 propext、Classical.choice、Quot.sound 时才通过，且仓库中没有任何模块使用 axiom、sorry、native_decide 等逃逸手段。
第一层核验是从零开始的 lake build：在 Lean 4.33.1 上、Mathlib 从源码编译，仓库全部 60,475 个模块构建通过，每条声明都经过 Lean 内核检查。README 记录了成本：96 并行任务下构建耗时 5 小时 32 分，峰值内存 153 GB。
第二层是 comparator 比对器（v4.33.0）。它把证明与只依赖 Mathlib 的挑战陈述逐项比对，确认被证明的陈述和用到的每个常量都与 Mathlib 自带的 FLT 陈述一致，再让整套证明（含 Mathlib）在内核中重放一遍，判定语是「Your solution is okay!」。这一层耗时约 14 小时 46 分，几乎全部是单核内核重放；README 建议为它预留 300 GB 内存（自家跑出的峰值是 230 GB）。
第三层是 nanoda 0.4.13——一个用 Rust 独立实现的 Lean 内核。它接受同一环境的导出文件，结论是「Checked 1052234 declarations with no errors（检查了 1,052,234 条声明，无错误）」。README 承认 nanoda 经过 Anthropic 自加的 4 个小补丁（一个加进度输出、三个加速定义相等性搜索），并声明这些补丁不增删、不削弱任何类型规则。
仓库被明确标注为「研究工件：不接受维护与贡献」，以 Apache-2.0 协议发布，版权归 Anthropic。NOTICE 文件致谢三个上游项目：Buzzard 领导的帝国理工学院 FLT 项目、leanprover-community 的 flt-regular 项目，以及 Mathlib；ATTRIBUTION.md 列出 106 个包含前两者材料的文件。
README 还附了约 390 MB 的离线 HTML 版本，为 29,511 条定理与 1,450 个定义模块各生成一页，可全程断网浏览。它承认这些 Lean 源码「为被检查而写，不是为被阅读而写」：名字由机器生成，除上游声明、文档字符串与引用外注释都被移除；名字与陈述不一致时，以陈述为准。
Buzzard：编译通过，数学上无新增
Buzzard 的人类 FLT 形式化项目于 2024 年启动（Anthropic 博客称该社区项目由他发起），受英国 EPSRC 资助。他的博客发布于官方 X 帖前约 20 分钟（UTC 18:30），标题是《FLT: Anthropic has beaten me to it》（FLT：Anthropic 抢在了我前面）。
他在博客里记下这次复核的具体情况：代码超过 1340 万行（高于 Anthropic 口径的 1300 万+），编译耗时接近 Mathlib 的 20 倍（96 核机器）；仓库大到 Lean 在文件间跳转都明显变慢，即便在 500 GB 内存的机器上——那是 Anthropic 提供给他用的。他还指出，这是 Freek Wiedijk 提出的 100 道形式化挑战清单的最后一题，它的完成意味着这个 20 年的基准就此收官。
对数学本身，Buzzard 的判断是：这份形式化「几乎什么也没告诉我们」。他自述对人类 FLT 证明正确的把握是 99.9%，数论界多数人是 100%——形式化让他比多数人更怀疑文献；在他看来，这份形式化忠实复述了 Wiles 证明的早期文献，没有增加内容。他同时澄清，这份证明走的不是他正在形式化的现代证明路线（Khare–Taylor 思路），而是 1995 年 Darmon–Diamond–Taylor 对 Wiles–Taylor–Wiles 论证的阐述。
他更看重自动形式化本身的可能性：「它告诉我们的是自动形式化领域什么是可能的。」如果几千页文献如今能被一个 AI 智能体群在 11 天内端到端形式化，那么对现代研究的实时形式化就近在眼前；「我们也会知道我对朗兰兹纲领现状的担心是否有道理——机器会检查它，并毫不留情地标记出不完整的论证。这会让我们保持诚实：有些论文默认了一些『专家都知道』的结果，我很想知道自己领域里那些重要结果的证明究竟假设了什么。」
Anthropic 博客引用他的另一段话说，这类技术会带来新工具，「在当前的数学文献中找出错误、减轻审稿人的负担」，也能用来严格核查 LLM 生成的数学——那在今天通常是一个极其昂贵的人力过程。
被抢先之后，人类形式化项目还在继续
Buzzard 专门回应了「人类项目是否还有必要」的问题。他列出自己向 EPSRC 承诺而尚未完成的事：向 Mathlib 提交现代数论基础对象的 pull request（正在进行），以及制作一份让人类能探索现代证明的动态文档。他猜测 Anthropic 不会做后者：对方大概会觉得自己该做的已经做完。
Anthropic 在博客里给出了下一步。它把这次流程当作例证：配上合适的框架，消费级 AI 订阅也能协作形式化重要结果——研究者用 3 个个人版 Claude Max 订阅计划，让智能体们在 Prove2Me 上仅 3 天就完成了 Vinogradov 三素数定理的形式化。博客还称，Anthropic 与其他实验室近期都在扩大对外部数学家的支持——免费与折扣订阅、研究额度——并为更大的科学项目提供专项资助，包括形式化其他大定理或改进 Lean 与 Mathlib；博客预期未来论文附一份形式化版本会成为常态，同时声明形式化证明不会取代人可读的阐述。
Anthropic 的仓库覆盖的是 Darmon–Diamond–Taylor 路线，而不是 Buzzard 正在形式化的现代证明（Khare–Taylor 思路）——这份仓库没有覆盖的部分，正是他的 EPSRC 项目要继续推进的。他在博客结尾这样比较两边的投入：「EPSRC 给了我 100 万英镑、5 年时间；Anthropic 只用了 11 天——但我在想，他们花的钱是不是比我还多。」