Anthropic 于 9 月 4 日发布了 Fermat's Last Theorem 在 Lean 4 中的机器验证形式化；GitHub API 显示该仓库创建于 UTC 14:21:04。外界流传的说法是 Claude 用 11 天证明了 Fermat's Last Theorem。仓库自身文件所描述的情况更窄一些，而且在某种意义上更有意思。
归属文件写了什么
该仓库附带一个 ATTRIBUTION.md，记录了106 个文件包含来自 Kevin Buzzard 领导的帝国理工学院 FLT 项目以及 flt-regular 项目的材料——“Definitions/ 下 54 个，P2M/Sol/ 下 52 个；以及复现 Mathlib 文本的 23 个文件”。其中数十行写着“whole file (100%)”。NOTICE 文件注明了借用时间：“Material was taken from the project's main branch as of 2026-05-21”。在迁移到 Lean 4.33 的工具链过程中，归属文件记录称它“留下了另外 41 个逐字节相同的文件”。
验证确实存在
但这些并不否定检查本身。README 显示全部 60,475 个模块都已构建，#print axioms fermat_last_theorem 只受三条标准公理约束，且没有任何模块包含 axiom、sorry、native_decide、unsafe 或 partial def。编译耗时 5 小时 32 分钟，使用 96 个并行任务，峰值内存为 153 GB。Anthropic 自身给出的数字是：1300 万行 Lean、最终证明中使用了 29,500 个中间定理，以及约 60 亿 输出 token。
既有表述哪里出了错
有三点。Claude 并没有证明什么新东西——这是一项对 1995 年 Darmon–Diamond–Taylor 对 Wiles–Taylor–Wiles 论证的阐释进行自动形式化的工作，而那一证明人类在 31 年前就已完成。它也不是完全没有人工参与：按 Anthropic 自己的统计，仓库的九分之一包含人类编写的 Lean 文本，其中有些是逐字复制。Anthropic 引用的那位数学家 Buzzard 也在同一天自己的博客上写道，从数学上说，这项 Anthropic 的工作“essentially nothing”，并称这项形式化“只是忠实地跟随了关于该证明的早期文献，并没有增加任何东西”。一些媒体还把它称为同类中最大的文件；但它有 60,475 个模块，而不是一个文件。
更诚实的说法依然很大
机器如今可以在不到两周的时间里，把数千页现有数学文献翻译成可由内核检查的形式，而这些工作是以多年志愿者 Lean 工作为基础的。这确实是关于翻译速度的成果，但不是关于数学发现的成果。README 甚至直接承认了剩余差距：“What no tool can check is that each intermediate theorem means what its name suggests.”