九月四日，Anthropic 在研究页写下一条听起来像科幻、实际是工程的句子：Claude 用大约十一天、基本自主地写出了费马大定理（FLT）的首个端到端、计算机可检查证明。Formalizing Fermat's Last Theorem 给出的量级很具体——约 1300 万行 Lean、最终用到 2.95 万个中间定理，一路上证明了约 3.03 万个；输出侧吃掉了约 60 亿 tokens，模型大致对标内部研究版、接近 Claude Fable 5.1。
这和前不久同一实验室在黎曼ζ函数零点上的工作形成刺眼对照。黎曼那条线的新闻价值在“新数学”；FLT 这条线的新闻价值在“旧证明被机器验完”。一个是开拓，一个是核账。核账听起来不性感，但数学共同体被审稿拖垮、被错误地基连坐的历史，往往比发现本身更长。
[1]机器把什么验完了
官方事实很清楚。证明路径大体跟着 Darmon–Diamond–Taylor 对 Wiles 证明的阐述走；人的介入主要是 Tianyi Peng 偶尔丢下的高优先级指令——“Jacobian as a scheme sounds high priority”一类。协作骨架不是聊天窗口，而是 Peng 与哥伦比亚大学合作者做的 Prove2Me：定理陈述被维护成 DAG，代理据此决定下一步；陈述与证明分文件，减轻 Lean 编译成本；每条定理附自然语言描述，方便检索复用。
早期失败并不少。代理一度跟丢全局状态、协作失效，那些废稿大约占最终证明非样板代码的 7%。换到 Prove2Me 与 Claude Code 多代理编排后，战役才收束。Lean 侧只用了三条标准公理；比较器确认陈述与 Mathlib 里的 FLT 陈述一致。Kevin Buzzard 审阅后称，这证明了自动形式化产物已经“robust enough to be built upon”。
同一套脚手架上，三人份 Claude Max 订阅、三天协作，还形式化了 Vinogradov 三素数定理——官方用它说明：大结果的协作形式化，不一定只能烧研究集群。完整证明已放在 GitHub。
[1]形式化到底解决什么痛
人类证明会跳步，Lean 不允许。人类证明站在几百年文献上，形式化只能站在已经入库的一小截。Buzzard 领衔的社区 FLT 项目原计划以年计，仅蓝图就有 86 页；Claude 用两周量级把它压成可机械检查的对象。
作者判断：真正被改写的不是“AI 会不会做数论”，而是“裁判工作能不能外包一部分给机器”。Perelman、Hales、弱哥德巴赫——接受一个正确证明，常常要数年。AI 产出速度上去之后，若不把形式化当成标配，审稿只会更堵。Anthropic 自己也写：他们并不认为形式化应取代人类可读论述，但可能是共同体跟上 AI 贡献的唯一可行方式。
[1]对谁有用，对谁暂时只是热闹
对数学家与形式化社区，这是工具可用性的一次压力测试：Prove2Me 这类 DAG 调度，比“多个 Claude 窗口各写一段”更接近可重复工程。对模型实验室，Lean 回路似乎也在反哺发现——官方称近期不少 Claude 结果在证明的同时并行形式化，模型用部分证明自检假设。对企业与普通用户，短期几乎无感；它更像科研基础设施新闻。
竞争面上，OpenAI 等同样在砸数学与证明助手。差异在叙事：Anthropic 愿意把“验证”写成正面议程，而不是只追排行榜上的新定理。谁先把“论文 + 可检查产物”变成默认交付，谁就更像在定义后 LLM 时代的数学信誉层。
[1]评论员看法
我认为把这篇读成“AI 证出了费马”是错的——Wiles 与 Taylor 等人证出了；Claude 做的是把一条已知、极难核验的人类证明，压成 Lean 可接受的形态。荣誉应记在形式化与编排，而不是改写数论史。
真正值得盯的有三件事：一是证明体积远大于 Mathlib，说明自动产物仍臃肿，后续压缩与社区接管成本未知；二是 7% 失败遗产仍进了最终仓库，提醒多代理数学仍是“带着伤疤前进”；三是当形式化成本降到 Max 订阅可及，错误与正确都会加速扩散——机器核账降低漏检，也可能让“先丢出形式化再补人类说明”变成坏激励。
和黎曼工作并读，实验室像在两条腿走路：一条腿去碰开放问题，一条腿把已有巨构焊进可检查底座。对我而言，后一条腿更能决定未来十年数学是否还信得过自己的地基。
[1]