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自主完成了人类数学最伟大证明之一”，则是一句需要加注脚才能成立的说法。
© 2026 Winzheng.com 赢政天下 | 转载请注明来源并附原文链接