Claude 在 11 天内用 Lean 形式化费马大定理
Anthropic 表示，Claude 生成了首个完整、经计算机验证的费马大定理证明，编写了 1300 万行 Lean 代码。
文章目录 · 11
Anthropic 于 9 月 4 日宣布，Claude 已生成首个完整、经计算机验证的费马大定理证明。该公司称，数十个 Claude 智能体在 11 天内大致自主地协同工作，生成约 1300 万行 Lean 代码，并证明了 30,300 个定理，其中约 29,500 个出现在最终证明中。
这并非传统数学意义上对费马大定理的新证明。Andrew Wiles 和 Richard Taylor 在 1990 年代完成了获认可的人类证明。Claude 所做的是将文献中既有的证明路径转换为一种形式语言，使其逻辑步骤能够由计算机检查。
这一区别很重要。该成果对于费马大定理是否成立，实质上没有增加新的知识；但它表明，AI 系统能够形式化一整套先进数学内容，而此前人们预计这需要多年专业工作。负责另一项形式化项目的伦敦帝国理工学院数学家 Kevin Buzzard 编译了 Anthropic 的代码，并运行了其比较器检查。他报告称，该证明验证无误。
一、Claude 形式化证明了什么
费马大定理指出，当整数指数 \(n\) 至少为三时，不存在满足 \(a^n+b^n=c^n\) 的正整数 \(a\)、\(b\) 和 \(c\)。这一陈述很初等，但已知证明依赖于涉及椭圆曲线、模形式、伽罗瓦表示、变形理论、代数几何和数论的复杂结果。
Anthropic 的代码库直接在 Lean 的自然数上表述最终定理。其陈述以正自然数 \(a\)、\(b\) 和 \(c\) 以及 \(n \geq 3\) 为条件，并证明该等式不可能成立。另一项最终检查则由该定理推出 Mathlib 中既有的费马大定理陈述。
该论证遵循 Frey、Serre、Ribet、Wiles 和 Taylor–Wiles 的工作，尤其是 Henri Darmon、Fred Diamond 和 Richard Taylor 于 1995 年作出的阐释。它利用假设存在费马方程解与一条 Frey 椭圆曲线之间的联系，随后应用模性和降层结果导出矛盾。
Buzzard 指出了构造中的一个重要细节。Anthropic 基于 Wiles 的路径处理素数指数 \(p \geq 17\)。完整结果纳入了此前已形式化的关于正则素数的工作，以覆盖其余情形。不过，所得 Lean 定理仍涵盖所有至少为三的自然数指数。
该成果也依赖于大量既有的人类工作。Anthropic 表示，它改编了伦敦帝国理工学院 FLT 项目、flt-regular 项目和 Mathlib 的材料。其署名文件列出了 106 个包含前两个项目材料的文件，以及 23 个复现 Mathlib 文本的文件。因此，这项成就是由 AI 主导、对既有形式化生态系统进行整合和扩展的成果，而不是脱离此前形式化数学独立创建的 1300 万行代码。
二、多智能体系统如何完成这一证明
Anthropic 最初发现，Claude 智能体能够证明单个结果，却会失去对整个项目的把握。智能体重复工作，未能有效复用已完成的定理，并且随着证明规模扩大而停止协调。失败尝试仍约占最终非样板代码的 7%。
成功的运行使用了 Prove2Me，这是由哥伦比亚大学 Tianyi Peng 及其合作者开发的开放协作形式化平台。Prove2Me 将项目表示为定理陈述的有向无环图。智能体可以选择尚未完成的节点、证明前提条件，并复用图中其他位置生成的结果。
该平台还将定理陈述与其证明分离。这一设计降低了重新编译的成本，并使系统能够修改或替换某项证明，而不会扰乱所有依赖它的陈述。附加在定理节点上的自然语言描述，也为智能体提供了另一种搜索不断扩展的库并识别有用依赖关系的方式。
一个基于 Claude Code 的多智能体框架在这次 11 天的运行期间协调了数十个智能体。据称，人类数学输入仅限于偶尔提供高层优先事项，例如引导智能体研究雅可比簇，或要求其完成与 Mazur 工作相关的某个定理。内部日志记录显示，根定理于 8 月 18 日被证明。
Anthropic 报告称，此次运行消耗了约 60 亿个输出 token。它使用了一种内部通用研究模型，仅被描述为与 Claude Fable 5.1 大致相当，因此确切模型和配置尚未公开。该公司尚未披露该项目的资金成本或计算成本。
完成后的开发项目在其可浏览文档中包含 29,511 个定理页面和 1,450 个定义模块。Anthropic 统计，整个运行过程中共有 30,300 个可由计算机验证的定理，其中包括最终依赖路径实际上并不需要的结果。
三、证明如何被检查
形式化证明的价值，取决于定理陈述、允许的假设以及验证过程是否受到控制。Anthropic 的代码库将项目固定在 Lean 4.33.1 和 Mathlib 4.33.0，并包含多层检查。
首先，项目从零开始构建。其 60,475 个模块均由 Lean 内核检查。最终定理恰好依赖于三条标准 Lean 公理：命题外延性、经典选择和商的可靠性。分发的证明模块不包含未完成的 sorry 占位符、新声明的公理、不安全代码、本地决策捷径或外部实现。
其次，项目使用 Lean Comparator，将已证明的定理与一个仅基于 Mathlib、单独提供的挑战陈述进行比较。该检查旨在确立该解证明的是同一命题、未使用未经批准的公理，并且被内核接受。比较器返回了接受判定。
第三，一个名为 nanoda 的独立 Lean 内核实现检查了导出的环境版本，并无错误地接受了 1,052,234 项声明。Anthropic 对 nanoda 应用了四个补丁：一个用于进度输出，三个用于加速定义相等性搜索。代码库称，这些补丁均未改变或削弱任何类型规则。
Buzzard 提供了最相关的外部确认。他在一台 96 核机器上编译了代码，并亲自运行了比较器。他将该代码库描述为超过 1340 万行，并表示其编译耗时接近 Lean 数学库的 20 倍。
复现每一项检查是可行的，但对硬件要求很高。Anthropic 记录的构建在 96 个并行任务下耗时 5 小时 32 分钟，内存峰值为 153 GB，并为 Lean 构建使用约 67 GB，另有最多 220 GB 可移除的生成 C 文件。其比较器运行耗时 14 小时 46 分钟，内存峰值为 230 GB。为第二个内核导出环境生成了一个 37.8 GB 文件。
这些检查确立了：在至少一个检查内核及其周边验证工具正确的前提下，精确的形式化陈述可由所列公理推出。它们并不会自动确立每个中间定理的机器生成名称都准确描述了其数学含义。Anthropic 通过一份证明路径文档应对这一局限，该文档将主要数学步骤映射到其精确的 Lean 陈述。
四、AI 辅助数学发生了什么变化
在此成果之前，费马大定理是 Freek Wiedijk 长期维护的 100 个著名定理形式化挑战清单中剩余的一项。伦敦帝国理工学院项目于 2024 年启动，获得五年资助，最初目标是将该定理归约为 1980 年代末已知的结果。该项目材料指出，完整形式化将需要翻译数千页非形式化数学内容。
Anthropic 的证明则端到端地到达了最终定理。Buzzard 强调，这并未让他的项目变得多余：帝国理工的工作正在为 Mathlib 开发可复用、可供人阅读的扩展内容，并遵循一条更现代的证明。Anthropic 将其代码库标注为不会维护且不接受贡献的研究成果。
因此，实际进展在于吞吐量。Claude 的智能体跨代数、调和分析、几何和数论组装了形式化定义和证明，其规模超过 Mathlib 的代码行数逾五倍。该结果表明，基于图的智能体系统能够维护依赖关系，并在规模大到超出单一模型上下文容量的形式化项目中协调工作。
该证明还展示了 AI 生成数学内容的验证路径。语言模型可以生成逻辑错误但措辞令人信服的自然语言论证，而 Lean 会拒绝无法通过类型检查的证明项。单独受控的定理陈述和比较器，进一步降低了智能体通过悄然削弱或改变问题而成功的风险。
这一机制并未消除对数学家的需求。人类仍须判断形式化陈述是否捕捉到预期概念，评估成果的重要性和表述方式，并维护可复用的库。不过，它可以将逻辑步骤的穷尽检查从人类审稿人转移给证明助手内核——前提是定义、定理陈述和可信验证边界均经过独立审查。
常见问题
Claude 发现了费马大定理的新证明吗？
没有。它将 Frey–Serre–Ribet–Wiles–Taylor–Wiles 文献中既有的证明路径形式化，使 Lean 能够检查每一步逻辑推理。
该成果是否经过独立验证？
Kevin Buzzard 编译了公开代码并运行 Lean Comparator，报告称其验证无误。代码库还记录了 Lean 和独立 nanoda 内核成功完成的检查。
哪个 Claude 模型生成了该证明？
Anthropic 尚未公布确切的公开模型。它将该内部通用研究模型描述为与 Claude Fable 5.1 大致相当。
研究人员可以复现验证吗？
可以，代码和说明以 Apache 2.0 许可公开。完整复现需要大量硬件资源，包括在某些验证阶段需要数百 GB 内存。
这份 1300 万行的代码库是否完全是 AI 新写的数学内容？
不是。AI 智能体生成并整合了大部分开发内容，同时建立在 Mathlib 以及伦敦帝国理工学院 FLT 和 flt-regular 项目此前的开源形式化工作之上。
参考来源
Share