11天、1300万行：Claude完成费马大定理首个计算机可验证证明，但自主二字值得细究

2026年9月4日Anthropic发布公告其内部研究模型在11天内写出费马大定理Fermat’s Last Theorem简称FLT的完整Lean形式化证明1300万行代码、30300个中间定理29500个进入最终证明、约60亿输出token。这是史上第一个经计算机完整核验的费马大定理证明。Anthropic官方博客称之为“有史以来最大规模的Lean证明文件”体积超过数学证明库Mathlib的五倍。在正式拆解这件事之前有必要先厘清一个常被混淆的概念这里发生的不是“AI发现了新数学”而是“AI将一个已有的人类证明转换成了机器可以一步一步核验的形式语言”。1995年英国数学家Andrew Wiles用129页的论文证明了费马大定理那是真正意义上破解350年悬案的数学发现。Claude做的是 形式化formalization ——把Wiles证明中涉及的代数数论、算术几何、伽罗瓦表示论等复杂推理链翻译成Lean证明助手可以自动检验正确性的代码。用一个粗略的类比这不是写一部新小说而是把一部已存在的小说逐字翻译成另一种语言并确保每个句子的逻辑在新语言中依然成立。技术机制不是一个Agent跑了11天Anthropic使用的平台是Prove2Me——一个开源的协作形式化平台其核心是用有向无环图DAG追踪定理之间的依赖关系。这种结构允许数十个Claude Agent并行工作一个子证明需要A定理和B定理就可以分配给不同Agent同步推进互不阻塞。Anthropic披露本次任务调用了“数十个”Claude Agent并发协作累计消耗约60亿个输出token。所谓“11天”指的是挂钟时间wall-clock time而非单一Agent顺序工作11天。这个区别意味着两件事一是任务的难度通过并行化被大幅摊薄二是整个系统的协调能力任务分解、依赖管理、子证明拼接是这次成功的核心变量而不仅仅是单次推理的质量。执行任务的模型被Anthropic描述为“大致相当于Fable 5.1”的内部研究版本具体参数规模未对外披露。人类研究员Tianyi Peng哥伦比亚大学在整个过程中提供了极少量的高层次指导例如一句“Jacobian as a scheme sounds high priority”其余部分由系统自主决策。Kevin Buzzard的双重身份帝国理工学院数学家Kevin Buzzard的反应值得重点关注因为他不只是一个旁观的评论者。2024年正是Buzzard发起了数学社区的集体形式化项目试图用人力逐步完成FLT的Lean化工作——这被认为可能需要数年时间。Buzzard看过Anthropic提交的证明后公开表示“这一非凡的自动形式化成就证明了费马大定理除数学公理外无需任何假设。其中涉及代数、调和分析、几何和数论的自动形式化AI自动形式化产物已经足够健壮可以作为后续工作的基础这个证明是多层次的。” 但他也间接承认了另一面Anthropic的GitHub仓库中有106个上游文件来自Buzzard自己领导的帝国理工FLT项目和Mathlib。也就是说Claude并非从零开始而是站在了数学社区多年积累的肩膀上再用AI的方式把剩余的缺口填满。“自主”的边界在哪里Anthropic公告中的“largely autonomously”大体自主地是整篇报道中最需要仔细读的四个字。据SiliconAngle等媒体报道Claude的第一次形式化尝试是失败的——成功需要加入Prove2Me这一第三方工具才得以实现。这说明所谓“自主”是在特定工具链和已有数学资产的框架内的自主而非白板起步的自主。这并不削弱成就本身的价值但它提醒我们当AI在一个“有据可查的人类知识体系”内执行长程任务时其可靠性表现与在开放域探索时大相径庭。29500个中间定理的正确组装依赖的是Lean语言本身的形式验证机制——每一步推理都由Lean内核实时检验错误无法传播。这是一个“有护栏的马拉松”而不是无边界的自由驰骋。AI数学竞赛的当前版图把这件事放在2026年AI数学领域的更大图景中才能看清其位置。今年早些时候OpenAI内部模型Astra公布了一批数学成果包括解决了困扰学界80年的Erdős单位距离问题Anthropic此前也披露另一个未发布模型在黎曼猜想上取得进展将已核验零点比例从41.6%进一步推进。这三个方向——Erdős组合问题、黎曼猜想、FLT形式化——分属“发现新数学”“推进已知边界”“验证已有数学”三种不同任务类型技术难度和意义完全不同。FLT形式化属于第三类最接近工程验证最远离数学创造但也最直接体现AI在长程、高精度、可验证任务上的执行能力。目前数学社区的一个关键问题是29500个中间定理中有多少会被Mathlib收录成为可供未来研究复用的模块如果大部分只是这次任务的一次性产物那AI的产出物与人类数学积累之间的对接管道仍然缺失。真正的里程碑是什么这件事的深层意义不在于AI“证明”了费马大定理那是Wiles在1995年做到的而在于它展示了一类新的AI能力组合在29500步相互依赖的逻辑推导中通过多Agent并行调度、DAG依赖追踪、Lean内核实时验证三者配合将长程任务的累积错误率控制在零。这种能力边界值得关注也值得警惕。形式化任务有一个人类自然语言任务不具备的关键属性每一步都有机器可判断的对错。这既是它成功的基础也是它的局限——现实世界中大多数任务没有Lean内核这样随时帮你兜底的验证机制。当同样的多Agent架构被用于没有实时验证层的任务时29500步无差错的表现能否复现目前没有公开数据回答。Anthropic本次的开放姿态值得肯定证明代码以Apache 2.0协议在GitHub公开Lean内核和nanoda独立内核均已验证通过第三方可以自行检验。这是一种少见的“说到做到”——不只是发布新闻稿而是把原始产物摆出来让任何人核查。学术界的真正检验将在接下来数月内随着数学家们深入审读这1300万行代码而逐步完成。在那之前“AI已经越过了形式化数学的里程碑门槛”是有据可依的判断而“AI自主完成了人类数学最伟大证明之一”则是一句需要加注脚才能成立的说法。本文首发于赢政天下 (https://www.winzheng.com/article/claude-fermat-last-theorem-lean-formalization-11-days)获取更多深度技术内容与资源欢迎访问官网。