Anthropic 那篇原文我逐条对了一遍，原帖的数字全对：1300 万行 Lean、30,300 条被证、29,500 条进最终证明、约 60 亿输出 token、模型大致对标 Claude Fable 5.1、走 Darmon–Diamond–Taylor 的简化版、只用 Lean 三条标准公理。
补几条原帖没给的。
【直引】项目牵头人是彭天翼（Tianyi Peng），清华姚班本科、MIT 博士、现哥伦比亚大学助理教授，Prove2Me 是他哥大团队做的。跑批是 8 月 7 日凌晨挂上去的，11 天是日历时长，几十个 agent 并行，不是单 agent 连续跑 11 天。人类输入只有偶尔几句，原话级别的指令是「Jacobian as a scheme 听起来优先级很高」「把 Mazur 定理推一推尽快做完」。
量级换一种算法更直观：Mathlib 大约 200 万行，1300 万行是它的 6.5 倍。Anthropic 自己只说「5 倍以上」。
证明和一份书面 walk-through 已经发在 GitHub 上，原帖没给这个出口。
一个历史细节适合放在开头讲。1908 年有人为费马大定理悬赏 10 万德国金马克（今天大约一两百万美元），第一年就收到 621 个错误证明。三百五十年里人类在这个命题上栽的跟头，比命题本身的难度更有教育意义。
真正该问的问题落在别处：这 1300 万行谁来读。【推论】29,500 条中间引理里，绝大多数不是 Wiles 论文里写出来的漂亮命题，是为了补人类省略掉的步骤硬堆出来的脚手架。人类数学家不会去读它，只看「Lean 编译器通过」这一个结果。证明的可信度，从「人读懂了所以信」挪到了「机器验过了所以信」。
Daniel Litt 那句「如果他们能形式化费马大定理，那么大概就能形式化任何东西」，【判断】后半句是推断，不是观测，别当成结论引。
下一根钉子：这 1300 万行里有多少条能被 Buzzard 团队搬进 Mathlib。搬不进去的那部分，就是机器可信还没转成人可用的那部分。