2026 年 9 月 4 日，Anthropic 公布一项里程碑：Claude 在约 11 天内，基本自主完成了费马大定理（FLT）的端到端、机器可检验形式化。最终产物约 1300 万行 Lean 代码，途中证明约 2.95 万条中间定理；Lean 核验后，仅依赖该系统的三条标准公理，且定理陈述与 Mathlib 中的 FLT 表述经比对一致。
这不是又一次“模型解出奥数题”的花絮。Wiles 1995 年的人类证明本身就花了数月人工核验；学界近年启动的 Lean 形式化工程，原本预期要数年。AI 把“把人类证明翻成机器可检语言”这件事，从长期科研项目压成了两周量级的 agent 战役。
发生了什么
费马大定理断言：对任意整数 $n>2$，不存在正整数 $a,b,c$ 满足 $a^n+b^n=c^n$。Andrew Wiles（后与 Richard Taylor 修补缺口）给出的证明长达约 129 页，依赖现代数论工具，远超费马本人时代的方法。
形式化（formalization）的目标，是把论证改写成证明助手（这里是 Lean）能逐步核验的代码——人类证明会跳过“显然”步骤，机器却要求每一步都显式。Anthropic 研究员 Tianyi Peng（其哥伦比亚大学合作团队也在做 AI 形式化工具）本想测试 Claude 能否推进 FLT 形式化；结果超出预期：在 Prove2Me 平台与 Claude Code 多智能体编排下，一支 agent 团队在不到两周内走完端到端路径，约消耗 60 亿输出 token；所用内部研究模型能力大致对标 Claude Fable 5.1。
早期尝试失败：agent 很快丢失项目全局状态、协作崩坏；失败产物仍贡献了最终非样板代码约 7%。切换到 Prove2Me 后才稳住——该开源协作平台用定理陈述的 DAG 引导下一步证明、拆分陈述与证明文件以加速编译，并用自然语言描述辅助检索复用。
为什么重要
Anthropic 特意区分：此前 Claude 在黎曼ζ函数相关工作上贡献的是新数学结果；这次 FLT 的新意在核验——像用计算器核对长计算一样，用机器核对长证明。Kevin Buzzard（帝国理工 FLT Lean 蓝图项目关键人物）审阅后称，这证明了自动形式化产物已“足够稳健、可被继续建设”，路径覆盖代数、调和分析、几何与数论等层。
对数学共同体，这意味着两件事同时加速：
- 存量纠错与审稿减负：把大段现代数学文献自动形式化，有望揪出语料库错误，并减轻 referee 对超长证明的人工负担。
- AI 产证的可信通道：当模型与“AI 辅助数学家”产出的声称证明越来越多，平行产出形式化证明，可能成为社区跟上产出节奏的可行方式——Anthropic 强调形式化不能替代人类可读阐述，但可成为信任基础设施。
公司还做了一个小对照：三套个人 Claude Max 订阅、仅通过 Prove2Me 协作，三天内完成了 Vinogradov 三素数定理的形式化——暗示在合适脚手架下，消费级订阅也可能扛起重大形式化战役。
边界与读法
需要压住过度解读：
- 这是形式化 Wiles–Taylor 路线，不是“AI 重新发现费马的神秘初等证明”。 证明沿 Darmon–Diamond–Taylor 对 Wiles 论证的整理展开，并适配了帝国理工 FLT 项目与 flt-regular 等既有人工蓝图片段。
- 规模不等于优雅。 约 1300 万行 Lean、体积超过 Mathlib 数倍，部分因为 Mathlib 本身精炼，而 AI 产物尚未压到社区可合入的形态；Buzzard 也把它定位为可继续建设的工件，而非终稿教科书。
- 人类仍在环内。 Peng 的高阶指令（例如优先推进某些定理）与平台脚手架，是失败跑与成功跑的分水岭；“自主”是相对多智能体编排而言，不是无人值守魔法。
- token 账单很重。 六亿级输出 token 说明：今天这条路径对算力与编排成本仍敏感，可复现性取决于平台、模型档位与工程纪律，而非单次聊天窗口。
观察
把 FLT 形式化读成“AGI 已到”会错过真正新闻点。真正新闻是：证明助手 + agent 图调度 + 大规模推理，正在把“数年蓝图工程”压缩成“以周计的战役”，并把数学信任问题从“谁有空读完 129 页”部分改写成“机器核是否接受这串推导”。
下一层竞争不在口号，而在三件事能否产品化：开源协作图（Prove2Me 一类）、可复用的中间定理库、以及把臃肿 AI Lean 压进 Mathlib 标准的工具链。谁先让“论文附带机器可检证明”成为默认交付，谁就更接近改写同行评议的成本结构。OpenAI 近期用前沿模型推进 Erdős 问题与理论 CS 开放题，Anthropic 则在ζ函数新结果与 FLT 形式化两条线上交替发力——数学正同时变成发现场与核验场。
结语
11 天、1300 万行 Lean、端到端 FLT：Anthropic 用一次可核验的战役，把自动形式化从愿景拉进了可引用的工程事实。接下来值得盯的不是更大标题，而是社区能否复现脚手架、压缩产物、并把“形式化并行于人类阐述”写进常规科研流程。