Anthropic称Claude代理团队用11天完成费马大定理的Lean形式化：重点不是“发现”而是机器核验

Anthropic 表示其 Claude 多代理团队在约11天内完成费马大定理的端到端 Lean 形式化并公开代码，生成约1,300万行 Lean 代码、29,511 个定理依赖。项目重点在于将现有数学证明转化为可由证明助手逐步核验的形式化代码，而非 Claude 独立发现新定理。

Anthropic表示，其Claude代理团队在约11天内完成了费马大定理（Fermat’s Last Theorem）的端到端、计算机可检查形式化，并公开了相关Lean代码。项目最终版本包含29,511个定理、约1,300万行Lean代码，证明依赖Lean的3个标准公理，没有使用未证明的占位符。

这并不意味着Claude独立发现了费马大定理，也不意味着人工数学证明被机器重新发明。费马大定理早在1995年已由安德鲁·怀尔斯（Andrew Wiles）在理查德·泰勒（Richard Taylor）的协助下证明。Anthropic这次工作的核心，是把既有的数学论证转化为一种能够由证明助手逐步检查的形式。

从费马的边注到怀尔斯的证明

费马大定理的命题很容易表述：当整数指数大于2时，不存在满足

[
a^n+b^n=c^n
]

的正整数(a)、(b)和(c)。据传，费马在《算术》一书的页边写下这个命题，并声称自己发现了一个“美妙的证明”，但边注空间太小，无法写下证明。

此后数百年间，数学家不断尝试解决这一问题。怀尔斯在1993年宣布证明后，同行在核查过程中发现了关键缺口；他随后与泰勒花了一年左右修补论证，最终在1995年发表了第一份被数学界接受的完整证明。相关证明长达数百页，使用了椭圆曲线、模形式和伽罗瓦表示等现代数学工具。

Anthropic官方技术说明称，此次形式化沿用了怀尔斯以及Taylor–Wiles的证明路线，并参考了Darmon、Diamond和Taylor对这一路线的整理。证明的核心结构包括：从假设存在费马方程的反例构造Frey曲线，再利用Mazur、Langlands–Tunnell和Ribet等定理所需的特例，完成模性提升和降层论证，最终得到矛盾。

11天内完成的究竟是什么

Anthropic在官方研究文章中说，Claude在8月启动的一次运行中，基本自主地连续工作了11天。数十个Claude代理并行负责定义概念、拆分任务、证明中间定理，并把已经完成的结果接入更大的依赖关系图。

官方发布的技术说明PDF进一步区分了几个数字：运行过程中，平台上的代理大约证明了30,300个定理；最终定理的依赖树经过重新检查后，包含29,511个定理。项目产生约1,300万行Lean代码，其中约1,050万行是在去除生成的样板代码之后的规模，且不包括Mathlib本身。

这项工作依赖了Lean的数学库Mathlib、帝国理工学院的FLT形式化项目，以及针对正规素数情形的flt-regular项目。Anthropic表示，最终代码中有106个文件改编自前述开源项目，并在代码仓库中列明了相关来源。

Anthropic公开的GitHub仓库将项目描述为“用Lean 4编写的、完整且经过机器检查的费马大定理证明”。仓库提供了证明路径、定理依赖关系和可离线浏览的HTML版本，方便研究人员逐步检查每个定理以及它在最终证明中的位置。

Lean检查的是逻辑链条，而不是数学直觉

形式化证明与普通数学论文的差别，在于它不能把“显然”“类似可得”或对已有结果的概括留给读者自行补全。Lean需要看到每一个足以构成逻辑链条的步骤，并由其内核判断这些步骤是否符合规则。

这使得形式化过程本身非常庞大。人类读者可以接受一页纸上的若干跳跃，但证明助手需要把定义、类型、引理和调用关系全部写清楚。此次项目的1,300万行代码，主要反映了把复杂数学论证翻译成可执行、可检查结构所需的工作量，而不是一份更长的新数学证明。

Anthropic表示，最终代码使用Lean的三个标准公理：propext、Classical.choice和Quot.sound，没有添加额外公理，也没有使用sorry等未证明占位符。仓库的FinalCheck.lean还检查了最终定理所依赖的公理集合，并将项目中的命题与Mathlib采用的费马大定理表述进行比较。

需要注意的是，“通过Lean检查”并不等于任何人都已经读懂了证明中的每一个数学思想。Anthropic在技术说明中也提醒，工具可以检查形式化代码是否满足类型和逻辑规则，但不能自动判断一个中间定理的名称是否准确描述了它的数学含义。这个问题仍然需要数学研究者阅读和解释。

多代理协作一度成为瓶颈

Anthropic对过程的描述也没有把项目写成一次平滑的自动化运行。官方文章称，早期尝试中，代理虽然取得了一些进展，却多次失去对项目整体状态的掌握，出现重复劳动，并停止有效协作。此前失败的工作最终贡献了约7%的非样板代码，但并没有直接完成项目。

转折点来自Prove2Me。这是由Anthropic研究员、哥伦比亚大学相关团队成员田一鹏（Tianyi Peng）及其合作者设计的数学形式化协作平台。平台把每个定理陈述及其证明组织成共享依赖图，使不同代理能够看到已经完成、正在等待或仍需拆解的任务。

Anthropic说，切换到Prove2Me并配合基于Claude Code的多代理框架后，团队才完成了这次运行。人类研究人员偶尔提供优先级和方向上的高层指示，例如要求优先推进Jacobian或Mazur定理，但公司称他们没有书写数学证明，也没有编写Lean代码，唯一例外是输入了最终目标定理的一行陈述。

这一点说明，项目的关键并不只是单个模型的数学能力。任务拆分、状态管理、依赖追踪、编译反馈和失败恢复，同样决定了多代理系统能否处理需要数天甚至更长时间的复杂工作。

与“AI发现新数学”是两条不同路线

Anthropic特意将这项工作与AI生成新数学的研究区分开来。费马大定理的数学结论和主要证明路线并非Claude首次提出；这次的新意在于，AI参与了把人类已经找到的证明系统地写成机器可验证形式。

这与此前有关AI辅助密码学研究的报道形成对照：密码学项目的重点是寻找此前未被识别的攻击路径，而费马大定理项目的重点则是把已有证明转化为可重复检查的代码。两者都涉及复杂的数学推理，但“提出新结果”和“验证既有结果”不能混为一谈。

New Scientist的交叉报道指出，形式化可以帮助数学界降低核查长证明的负担。人工审阅一份跨越多个数学领域的证明，可能需要数月甚至数年；证明助手则可以在明确的形式系统中逐步检查代码是否成立。

不过，机器核验并不能取代人类可读的数学解释。研究者仍然需要说明定理为什么重要、证明采用了什么策略，以及每个中间结果在整体论证中扮演什么角色。更现实的方向可能是让两种形式并行存在：一份供人类理解的数学叙述，加上一份供机器核验的形式化证明。

速度提升也带来了新的问题

帝国理工学院数学家凯文·巴扎德（Kevin Buzzard）在Anthropic文章中称，这是一项“非凡的自动形式化成就”。他认为，项目跨越代数、调和分析、几何和数论等领域，说明AI生成的形式化成果已经足够稳健，可以作为后续数学工作的基础。

巴扎德团队自2024年起推动费马大定理的Lean形式化，原本预计需要多年完成。Anthropic此次运行在不到两周内完成，显示出大型语言模型和多代理工具可能改变形式化数学的时间尺度。

但速度并不自动等于可复用性。Anthropic承认，当前代码还没有整理成可以直接并入Mathlib的形式。代码规模庞大、部分内容由机器生成，后续仍需要人类研究者理解、重构、维护并决定哪些通用结果值得纳入公共数学库。

项目本身也消耗了大量计算资源。Anthropic称，这次运行使用了约60亿个输出token，并依赖一个内部研究模型，其能力大致相当于Claude Fable 5.1。这样的成本意味着，11天这一数字不能简单理解为任何个人或普通计算环境都能复制的结果。

更广泛的问题是，当AI能够以更低成本生成大量数学候选证明时，数学界是否有足够的工具和人力进行筛选、解释和维护。形式化可能缓解“证明是否成立”的核验压力，却不会消除“证明是否值得研究”以及“结果是否被正确理解”的判断工作。

形式化可能成为AI数学研究的基础设施

Anthropic的判断是，随着AI参与数学研究的程度提高，形式化证明可能从专门项目变成研究成果的标准配套。对于AI生成的新定理或新证明，Lean一类的证明助手可以提供一个明确的通过或失败信号；对于人类已发表的数学文献，自动形式化则可能帮助发现长期未被注意的漏洞或不一致。

费马大定理案例的意义，因而不在于Claude“解决了一个已经解决的问题”，而在于它展示了一种新的研究分工：人类提供理论路线、数学语义和优先级判断，AI代理负责大规模的形式化、拆解和修补，证明助手则对最终逻辑链条作出机械检查。

这条路线仍有明显限制。形式化库的覆盖范围、代码的可维护性、生成结果的数学可读性，以及运行成本，都决定了它能否从一次引人注目的演示变成日常研究工具。Anthropic公开的代码和技术说明，为外部研究者提供了复查和复现的入口，但它们也清楚表明：这是一项形式化工程的里程碑，而不是一项由Claude独立发现的新数学定理。