费马大定理被机器验完了，Buzzard 为什么还要继续做？

先说结论

AI 把一道大题做完，能不能顺便把一个领域的基础设施建好？费马大定理的自动形式化，让这两个目标之间的距离变得具体。

9 月 4 日，数学家 Kevin Buzzard 在个人博客祝贺 Anthropic 抢先完成任务，却解释自己为何还要继续：他的项目还要向公共数学库贡献基础对象，并制作让人探索现代证明的动态文档。终点的勾打上了，通往那里、供后来者使用的路仍有工作要做。Buzzard 原文

事情是怎么发生的

同日，Anthropic 公布费马大定理的完整 Lean 形式化，称 Claude 在十一天内基本自主完成。这里的突破是把已有数学证明转成机器可检查的形式；公司明确区分了这项工作与发现新数学。项目使用内部研究模型、多智能体协作工具，也借用了人类已有的形式化成果。官方说明

Buzzard 的回应有分量，因为他自己就在做费马大定理的形式化。他报告亲自编译代码并运行 comparator 检查，结果通过；同时指出，这份成果沿用的证明路线与自己推进的现代版本不同。因此，十一天不能直接拿来除以人类项目的几年，算出一个替代倍数。本人核验与说明

为什么重要

这件事把 AI 交付物分出了两个层次。第一层是一个可检查的结果：在给定形式系统里，结论能否成立。第二层是可持续使用的知识：概念是否组织得好，别人能否找到需要的部分，换一道题还能不能接着用。

两层都重要，却不能互相代替。一座桥通过承重测试，并不自动意味着施工图清楚、部件通用、维护方便。同样，一份形式证明通过检查，也没有回答它是否适合成为公共库的一部分。

由此看，AI 产业的交付标准值得多加一问：完成这次任务之后，下一位使用者的成本降了多少？如果每次都得重新生成、重新整理，产量增长未必能积累成知识资产。

站得住与站不住的地方

Buzzard 的区分站得住。把“已完成”与“适合继续建设”分开，能避免用单次成功掩盖长期维护成本。他也没有否认突破：他期待自动形式化减轻审稿负担，把文献中依赖专家默契的隐含假设暴露出来。这是对未来用途的判断，还不是普遍实现的结果。原文讨论

但不能反过来断言，人类可读性不足就让机器成果没有价值。专用证明可以先承担核验工作，随后再被压缩、整理和复用。Anthropic 也明确表示，形式证明不应取代人能理解的论述；双方在这一点上并无根本冲突。官方立场

真正未解的是经济账：后续整理需要多少人工，能否持续更新，以及投入这些成本后，比原来的工作方式节省多少。单个里程碑还回答不了。

接下来该盯什么

值得看三个后续：产物有多少进入公共库；其他团队复用了哪些部分；面对新的结果，能否同时交付机器检查与清楚解释。

如果这三件事接上了，AI 才是在持续扩充公共知识。否则，它仍可能是一位出色的解题者，却把整理书架的工作留给了别人。