9月5日消息,Anthropic 宣布其 AI 模型 Claude 完成了费马大定理的首个端到端计算机可校验证明,全部 Lean 代码已在 GitHub 开源。费马大定理断言当 n 大于 2 时方程 aⁿ+bⁿ=cⁿ 没有正整数解,1995 年由 Andrew Wiles 首次证明。需要先说清边界:这件事不是 AI 重新证明了费马大定理。Anthropic 在公告中明确,与 8 月黎曼猜想下界这类产出新结果的工作不同,这次突破的是"验证",即把一个已成立 30 年的人类证明完整翻译成机器可以逐步检查的形式。 做成了什么:把已知证明变成机器可检的代码
Claude 在 11 天里基本自主地工作,共写下 1300 万行 Lean 代码,证明了 3.03 万个定理,最终证明使用了其中 2.95 万个。Anthropic 称这是费马大定理首个完整的机器校验证明,体量是 Lean 社区核心数学库 Mathlib 的五倍以上。
可信度由几层检查支撑。整个证明只依赖 Lean 的三条标准公理,没有使用任何未证明的占位;Lean 官方的 comparator 工具确认证明的命题与 Mathlib 中费马大定理的标准表述完全一致;一个用 Rust 编写的独立内核 nanoda 复核了全部 105 万余条声明,没有报错。仓库同时附带约 390 MB 的网页版证明浏览文件,可以离线逐层查看每个定理的依赖关系。仓库标注为研究产物,不维护也不接受贡献,以 Apache 2.0 协议发布。
怎么做到的:内部研究模型、多智能体与 Prove2Me
完成这项工作的不是任何公开版本的 Claude。Anthropic 披露,实际运行的是一个"大致相当于 Claude Fable 5.1 的通用内部研究模型",通过基于 Claude Code 的多智能体框架协作,全程消耗约 60 亿输出 token。 过程并非一次跑通。最初的尝试中,智能体群很快丢失项目状态、协作失效;转向 Prove2Me 之后项目才走上正轨。Prove2Me 是 Anthropic 研究员 Tianyi Peng 与他在哥伦比亚大学的合作者设计的开放协作平台,用有向无环图维护定理之间的依赖关系,让几十个 Claude 智能体可以并行认领证明任务。整个项目由 Tianyi Peng 发起,人类的数学输入限于少量高层指令,例如提示某个定理应该优先完成。平台记录显示,根定理在8月18日凌晨闭合,到9月4日才对外发布。早期失败尝试产生的代码约占最终证明非模板行数的 7%。
站在谁的工作上
Claude 的证明走的是 Frey、Serre、Ribet、Wiles 与 Taylor-Wiles 的经典路线,具体遵循 Darmon、Diamond 和 Taylor 的简化版表述。证明直接改用了两部分人类工作:帝国理工学院 Kevin Buzzard 领导的费马大定理形式化项目——这个由数学家社区推进的项目 2024 年才启动,原本预计耗时数年——以及 Kummer 定理的 flt-regular 项目和 Mathlib 库。仓库的署名文件逐一列出了来自这些项目的百余个文件及原作者。
Buzzard 本人审阅了这份证明。他评价说,如果自动形式化费马大定理现在就能做到,那么自动形式化现代数学文献就迈出了一大步,这类技术可以筛出数学文献中的错误、减轻审稿人负担,也让严格检查 AI 生成的数学成为可能。这段评价由 Anthropic 收录在公告中。
形式化这个最慢的环节,开始可以被 AI 批量承担
数学证明的信任链条里,验证一直是最慢的一环:Wiles 的证明在发表前被审稿人抓出漏洞,又花了一年才补上;学界对形式化 Wiles 证明的共识预期是以年计。这次 11 天完成,加上 Anthropic 披露的另一组对照——用三个个人版 Claude Max 订阅,智能体经 Prove2Me 协作,3 天形式化了 Vinogradov 三素数定理——指向同一个变化:把人类数学转成机器可检形式的工作,开始可以被 AI 批量承担。
但这只是形式化能力的里程碑,不是 AI 做出新数学的证据,Anthropic 的公告本身也是这样定性的。Buzzard 所说的"自动形式化现代数学文献"目前仍只是方向;消费级订阅能否稳定复现这类工作,官方只给过一次小规模实验,目前没有更多依据。