Claude × 费马大定理：11 天、约 1300 万行 Lean 的端到端形式化

Anthropic 公开了一件更偏「研究基础设施」的事：Claude 在约 11 天里，基本自主写出了费马大定理（FLT）的首个端到端、机器可检 Lean 形式化证明。 先把边界说清：这不是推翻或重写 Wiles 的新数学结果，而是把已知证明翻译成证明助手能逐步核验的形式。Wiles 1995 年的证明曾让人类审稿花很长时间；形式化的价值，是把「信任链条」交给 Lean 的内核。

一、公开数字

• 约 1300 万行 Lean（官方称规模超过 Mathlib 五倍以上；另有「约 1050 万行不含生成样板」的口径）
• 途中证明约 3.03 万个定理，最终证明用上其中约 2.95 万个
• 只依赖 Lean 的三条标准公理；无 sorry 占位
• 定理陈述经 comparator 与 Mathlib 中的 FLT 陈述对齐
• 另经独立 Lean kernel 实现核对
• 消耗大约 60 亿 output tokens；底层是接近 Claude Fable 5.1 能力档的内部研究模型 证明路径大体跟随 Darmon–Diamond–Taylor 对 Wiles / Taylor–Wiles 路线的整理，并致谢/借用了 Imperial College FLT 项目与 flt-regular 等社区工作（公开材料提到约 106 个文件有改编致谢）。

二、工程关键：Prove2Me

早期多 agent 一度失联、协作崩掉——单个 agent 能推进局部，却跟丢全局依赖。切到 Prove2Me（Tianyi Peng 与哥伦比亚大学合作者等设计的开放协作平台）加上 Claude Code 式 harness 后才跑通。 Prove2Me 做了三件很「工程」的事：

1. 维护定理 DAG：agents 据此决定下一步证明什么，缓解记忆退化，并支持并行
2. 陈述与证明分文件：链接独立维护，加快 Lean 编译、降低资源消耗
3. 自然语言检索复用：后续 agent 能搜到已有结果，而不是重复推导

三、第三方核对与「可复用」信号

Kevin Buzzard（长期主导人类侧 FLT Lean 项目的数学家）下载仓库自行编译核对后公开承认被追上，并评价这类 artefact 已「稳到可以继续往上盖」。正式仓库见 Anthropic 公开的 FLT Lean 项目（github.com/anthropics/fermats-last-theorem）。 Anthropic 自己也做了小实验：用三份个人 Claude Max，经 Prove2Me 协作，约三天形式化了 Vinogradov 三素数定理相关材料——暗示「大定理形式化」未必只能是实验室特权。

四、为什么值得写

AI 在数学里最干净的角色，也许不是抢发现，而是把验证成本压下来，让共同体跟得上越来越多的 AI 辅助证明。FLT 这次的看点，不在「又证了一道题」，而在：Wiles 级巨证明可以被自动翻成 Lean，并且经独立编译核对。