1637 年,费马在一本书的页边写下断言:当 n>2 时,不存在正整数满足 aⁿ+bⁿ=cⁿ。这个「页边太窄写不下」的猜想困扰数学界 350 多年,直到 1995 年 Andrew Wiles 才给出首个证明——129 页,数月才核验完。Anthropic 9 月 4 日发布了这条定理的首个完整机器验证证明:Claude 多智能体用 11 天写出 1300 万行 Lean 代码,由证明助手内核逐行检查通过。
十一天,1300 万行 Lean
形式化由 Anthropic 研究员 Tianyi Peng 发起,他在哥伦比亚大学的研究组研究 AI 形式化工具。项目本想测试 Claude 能推进多少,结果远超预期:11 天里 Claude 基本自主工作,累计证明 30,300 个定理,最终采用 29,500 个;代码量是数学界主力库 Mathlib 的五倍以上;全程消耗约 60 亿输出 token,内部研究模型,能力与 Claude Fable 5.1 大致相当。官方日志显示,8 月 18 日凌晨 Lean 把 FLT 根定理标记为 PROVED。
真正的功臣是协作架构
官方复盘里最值得工程师看的细节:agent 们最初并不成功,很快丢失项目状态、停止有效协作。转折点是切换到 Prove2Me——Tianyi Peng 与哥伦比亚合作者开发的开放协作形式化平台。它维护一张定理依赖的 DAG 图,让 agent 自己决定下一步证什么,同时对抗记忆退化、支撑多 agent 并行;定理语句与证明分文件存放以加速编译。数十个 agent 在 Claude Code harness 上协作,人类输入只剩「尽快推进 Mazur 定理」这类高层指令。
为什么重要
Anthropic 强调:新的东西是「验证」,不是新数学——类似用计算器核对算术,对象换成人类最难的一批证明。Wiles 1993 年宣讲后,审读数学家两个月就发现关键漏洞,他又花一年、与 Richard Taylor 合作才补全。形式化 FLT 此前公认要以年计——帝国理工 Kevin Buzzard 2024 年发起社区项目,仅初始阶段 blueprint 就有 86 页。Claude 的证明走 Darmon-Diamond-Taylor 简化版路线,Buzzard 审阅后评价:autoformalization 工件已经「robust enough to be built upon」。
冷静看的部分
其一,「基本自主」不等于无人驾驶,方向性决策仍在人类手里;官方也承认 1300 万行「远超必要长度」——这份证明为机器检查而写,不为可读性。其二,仓库标注为研究工件,不维护、不接受贡献。其三,验证本身是硬的:GitHub 上全部 60,475 个模块在 Lean 4.33.1 下从零构建通过,独立工具 comparator 确认所证定理与 Mathlib 的 FLT 陈述一致。另有个对照实验:三个个人版 Claude Max 订阅协作三天,就形式化了 Vinogradov 三素数定理——形式化门槛正从研究院预算滑向个人订阅。
所以呢。意义不在费马——定理 1995 年就证完了——而在信任的机械化:当 AI 越来越快地产出「证明」,人类审读注定跟不上,机器验证成了数学界扩容信任体系的可行路径。Anthropic 判断,论文附带形式化证明会变成常态;对 AI 行业,这也是多智能体端到端交付的展示——协作架构比单模型能力更是主角。
原文: anthropic.com/research/formalizing-fermats-last-theorem | 仓库: github.com/anthropics/fermats-last-theorem