1637 年，费马在一本书的页边写下：我找到了一个绝妙的证明，可惜这页边太窄，写不下。这句话为难了数学界 358 年。1995 年 Wiles 补完证明，《数学年刊》刊出，正文 129 页。2026 年 9 月 4 日，Anthropic 公布：他们的内部模型把这条定理在 Lean 里完整形式化了——11 天，60,474 个文件，一千三百多万行代码。
先做个尺度换算。Wiles 的证明打印出来大概是一块砖。这次的产物是一面墙：96 核、512 GB 内存的机器全量编译要 5 小时 52 分，约为 mathlib（全球 Lean 社区二十年攒下的数学库）编译时间的近 20 倍。验货的 Kevin Buzzard 原话：”It is a gigantic proof (over 13.4 million lines of code)”。
timeline title 一条定理的 389 年 1637 : 费马页边写下绝妙证明的预告 1993 : Wiles 剑桥三场演讲 1994 : 审稿发现漏洞 与 Taylor 一年补洞 1995 : 数学年刊刊出 129 页 2024 : Buzzard 拿百万英镑立项要亲手形式化 2026年8月7日 : 机器开跑 2026年8月17日 : 深夜十点根节点显示 PROVED 2026年9月4日 : 仓库公开 博客发文
干活的到底是谁
官方口径：一台”通用内部研究模型，大致与 Claude Fable 5.1 相当”，几十个 agent 跑在 Claude Code 改造的多智能体框架上，平台是哥伦比亚大学 Tianyi Peng 团队的 Prove2Me。论文里写得更干脆——人类没写任何数学、任何 Lean，除了目标定理那一行陈述。8 月 7 日开跑，8 月 17 日深夜 10 点 00 分 57 秒，FLT 根节点翻成 PROVED。机器自己在日志里记了一句：”Historic moment for this campaign.”
验货的人，是最有资格难过的人
Kevin Buzzard，帝国理工教授，拿了一百万英镑、五年期的 EPSRC 经费，计划带人类社区亲手形式化 FLT。Anthropic 的邮件到的时候，他正在 Green Man 音乐节，看完标题判定为民科来信。三天后他在伦敦一家咖啡馆的 Instagram 上看到了正式消息。
然后他做了一件对的事：下载公开仓库，亲自编译，跑 Lean FRO 的 comparator。博客标题起得认赌服输——《FLT: Anthropic has beaten me to it》。正文那句是全篇的钉子：”I’ve compiled the code base and run comparator on it — it checks out.”
信任链不止一层。第二个独立内核 nanoda（约五千行 Rust 重写的 Lean 内核）重新接受了全部声明；整棵证明树只依赖 Lean 的三条标准公理，零 sorry；comparator 确认证明的命题与一个只 import mathlib 的参考陈述严格一致——防的是偷换命题。HN 上最锋利的质疑是”1340 万行 agent 代码会不会钻内核空子”，今年 Collatz 事件确实出过这种前科。Buzzard 的回应笨拙但扎实：他逐行读了那约一百行不属于数学定义与证明的代码，防的就是这种作弊。
走的是 1995 年的老路
flowchart LR
A[假设反例
弗雷曲线] –> B[Mazur 模 p 不可约]
B –> C[Langlands 与 Tunnell
p 等于 3 处理]
C –> D[3 到 5 切换]
D –> E[R 等于 T 模性提升]
E –> F[Ribet 降阶到级 2]
F –> G[级 2 无尖点形式
矛盾]
G –> H[FLT 得证]
机器走的路线是 Darmon–Diamond–Taylor 1995 年的早期表述，没走现代证明。Buzzard 点破关键：”形式化忠实跟随早期文献，没有添加任何东西。”数学是 Wiles 的。机器的贡献是把 129 页人间证明翻译成机器可查的形式——而且翻译得极其浪费。
xychart-beta title “代码行数 万行” x-axis [“Mathlib 约200”, “FLT 仓库 1340”] y-axis “万行” 0 –> 1500 bar [200, 1340]
Anthropic 自己说 1300 万行（去掉生成样板 1050 万），Buzzard 数出 1340 万，Claude 自评 1350 万——同一个仓库，三个口径。都指向一件事：这面墙是六个 mathlib 那么大。
诚实的星号，一个都不能少
这份成果自带说明书没印在新闻里的部分：
一，机器只证了指数 p ≥ 17 的情形。小素数由人类 2025 年的 flt-regular 项目补齐——最小的非正则素数是 37。细节里还藏着较真：该项目作者 Brasca 澄清，3、5、7、11、13 的正则性是在仓库里手写证明的，没有引用现成结论。
二，中间定理全是”特供版”。论文自己承认，仓库里的”Ribet””Wiles””Mazur”都是证明所需的特殊情形，limitations 文档明言不可当作一般经典定理引用。
三，代码品质够不着 mathlib 门槛：900 多个文件超出 mathlib 的 1500 行上限，31% 的字节是生成样板，五分之二的定理陈述是重复声明。
四，Wiedijk 的”百大形式化挑战”清单——FLT 是其中最后一项——官方页面到昨天还停在 99%，斜体的 FLT 等着更新。跑完比赛的计分牌，自己还没翻页。
这堵墙塌了之后
Buzzard 说了句看似扫兴的实话：”数学上这项工作几乎什么也没告诉我们。”他本来就 99.9% 确信 FLT 是对的。值钱的是基建：autoformalization 从辅助工具变成了能独立完成研究级对象的流水线。他的项目照跑，换现代路线继续。
成本对照有点好笑。Buzzard：一百万英镑，五年。Anthropic：约 60 亿输出 token，11 天，HN 上有人按 API 价估了 10 到 30 万美元。Buzzard 自己调侃：”我确实怀疑他们花的钱更多……”
同期还有个不起眼的 side experiment：三个消费级 Claude Max 订阅，三天，形式化了维诺格拉多夫三素数定理。费马这堵墙塌了，下一张该列什么清单——现在还没人写出来。我不知道答案，只知道这个问题比上周难回避得多了。
参考：Anthropic 博客 ｜ Buzzard 验货原文 ｜ 公开仓库 ｜ Wiedijk 清单