Anthropic 于 2026 年 9 月 4 日表示，Claude 基本自主地工作了 11 天，写出了费马大定理的证明。公司称，这是该定理首个经计算机检验的完整证明。证明用 Lean 写成。Lean 是一种证明助手，也就是能逐步检查证明的软件。[1]

据 Anthropic 介绍，数十个 Claude 智能体写下约 1300 万行 Lean 代码，证明了约 29,500 个中间定理，供最终证明使用。这些智能体使用的是一个内部模型，公司称该模型大致相当于 Claude Fable 5.1。证明沿用的是 Henri Darmon、Fred Diamond 和 Richard Taylor 对 Andrew Wiles 证明的简化版本。Anthropic 称，人类在数学上的参与仅限于其研究员 Tianyi Peng 偶尔给出的高层指示。智能体通过 Prove2Me 协同工作，这一平台由 Peng 在哥伦比亚大学的研究组开发。这份证明还改编了伦敦帝国理工学院一个项目的部分内容。该项目由 Kevin Buzzard 领导，目标是把这一定理形式化，即写成经计算机检验的证明。[1]

证明已在 GitHub 上公开。按默认设置，只要定理依赖了 Lean 三条标准公理以外的公理，构建就会失败。根据 README，Lean 的内核检查了每一条声明。内核是 Lean 中负责接受或拒绝证明的核心程序。README 还称，comparator 工具确认所证明的命题与一条参考命题相符，后者用 Lean 的主要数学库 Mathlib 写成。第二个独立内核 nanoda 在打上补丁后也接受了这一证明，Anthropic 称这些补丁不会改变它的类型规则。README 称，只要信任这些内核和检查工具，上述检查就确立了最终定理。但它也指出，没有任何工具能检查每个中间定理的含义是否与其名称相符。重复这些检查对计算资源要求很高。Anthropic 以 96 个并行任务运行构建，耗时约五个半小时；运行 comparator 耗时近 15 个小时，内存峰值达 230 GB。[2]

Buzzard 于 9 月 4 日撰文称，他已编译代码并运行了 comparator，结果没有问题。他补充说，这项工作在数学上基本没有给数论学家带来新东西，因为他们原本就信任这一证明，而这次形式化遵循的也是该证明的早期文献。他写道，这项工作的意义在于展示了自动形式化能够做到什么。[3]

来源

  1. Formalizing Fermat's Last TheoremAnthropic · 2026年9月4日
  2. Fermat's Last Theorem in Lean 4 (anthropics/fermats-last-theorem README)GitHub · 2026年9月15日
  3. FLT: Anthropic has beaten me to itXena Project blog (Kevin Buzzard) · 2026年9月4日

核查或更正本页

更正
提交更正请求 · 在 GitHub 编辑源文件 · 更正政策
验证记录

下方摘要可以说明你读到的文字是否与公开的源文件一致，但不能说明报道内容本身正确。这一摘要在构建时根据本页的 Markdown 源文件计算，并列入站点清单。

49a75f85159639de7f7391d0f9fd6a2d33737de5b7c872021321242fe436b905

查看源文件 · 清单