主要证据
- Formalizing Fermat's Last TheoremS2 · 官方机构来源 · 官方公告 · 2026-09-04
- Fermat's Last Theorem in Lean 4S1 · 主要研究来源 · 形式化工件 · 2026-09-04
Anthropic 发布由 Claude 生成的费马大定理完整 Lean 形式化
Claude Agent 使用 Anthropic 的 Prove2Me 工作流构建形式化子问题依赖图，并将其扩展为数百万行 Lean 代码。仓库沿用经典的 Frey–Serre–Ribet–Wiles–Taylor-Wiles 路线，并公开定理依赖图、来源归属和可复现验证流程。
发生了什么？
Anthropic 将该发布描述为费马大定理首次完整的计算机检查形式化。公开 Lean 仓库陈述了标准定理，在构建包中不包含被承认的证明缺口，并报告已通过 Lean、comparator 以及第二个 Rust Lean 内核的检查。
为什么重要？
该事件的重要性主要在自动形式化与证明工程，而不是发现费马大定理的新证明。它检验了多 Agent 系统能否组装并验证一个极其庞大的既有数学论证，同时保持机器可检查的正确性。
重要性说明：该发布展示了规模异常巨大的 AI 驱动形式化：Claude 在 11 天内大部分时间自主工作，将既有的 Wiles 与 Taylor-Wiles 论证转化为可由证明内核检查的 Lean 产物，目标是一个现代数学标志性定理。
历史脉络
证据与状态一览
- 重要性
- H1 · 历史里程碑
- 验证状态
- 已有独立佐证
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 已独立复现
贡献与验证
- 数学新颖性
- 已知结果形式化
- 接口
- 形式化, 符号, 混合
- AI 贡献
- Claude Agent 生成了大部分 Lean 形式化内容、分解证明义务，并根据 Lean 反馈迭代修复代码；证明内核负责判定最终形式项是否通过类型检查。
- 人类贡献
- 底层数学来自最终由 Wiles 与 Taylor-Wiles 完成的费马大定理研究，以及后续阐释和开放 Lean 数学库。Anthropic 研究者设计并编排 Agent 工作流、选择来源、整合既有形式库，并记录验证和归属信息。
- 验证状态
- 已有独立佐证 · E3 · 可检查工件 · 已独立复现
- 最后审阅
- 2026-09-11
技术细节
- 系统
- claude, prove2me, lean, mathlib
- 机构
- anthropic, imperial-college-london, lean-community
- 数学问题
- fermats-last-theorem
- 方法
- multi-agent, autoformalization, formal-theorem-proving, lean, proof-dag
全部来源与工件
- Formalizing Fermat's Last TheoremS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-10
- Fermat's Last Theorem in Lean 4S1 · 主要研究来源 · 形式化工件 · 访问于 2026-09-10
- FLT: Anthropic has beaten me to itS3 · 独立学术来源 · 独立分析 · 访问于 2026-09-10
- Anthropic AI formalizes proof of Fermat's last theorem — a milestone for mathematicsS4 · 可信二手来源 · 媒体报道 · 访问于 2026-09-10
验证历史
- 2026-09-04 · 部分核验 · E3 · 可检查工件
Anthropic 公开完整 Lean 产物；其验证文档报告了从头 Lean 构建、针对标准 Mathlib 挑战陈述的 comparator 重放，以及独立 nanoda Lean 内核实现的通过结果。
- 2026-09-04 · 部分核验 · E3 · 可检查工件
Kevin Buzzard 独立报告称已编译公开代码库并成功运行 comparator；他还人工检查了并非数学定义或定理证明的代码，以排查可疑机制。这支持将 formal assurance 记为 `independently_replayed`，但其本身不自动触发 Chronicle 的 `independently_verified` 编辑状态。
- 2026-09-07 · 部分核验 · E3 · 可检查工件
Nature 独立报道了该形式化，并引用数学家对其规模与意义的评价。AI4Math Chronicle 在未单独审核产物重放与数学忠实性之前，不授予 independently_verified 状态。
- 2026-09-10 · 已有独立佐证 · E3 · 可检查工件
按 Chronicle 的事件级 verification 语义，Kevin Buzzard 的独立编译与 comparator 重放，加上 Nature 的独立报道，已经对该事件的核心描述形成实质性独立佐证。该状态核验的是事件记录与公开形式化产物，而不是由 Chronicle 对所有底层数学依赖或主张的最终正确性作裁决。
更正
当前没有记录的更正。