来源 · GitHub（anthropics/fermats-last-theorem）
A complete, machine-checked proof of Fermat's Last Theorem in Lean 4
来源
原始文章、报告或对话- 出处
- GitHub（anthropics/fermats-last-theorem）
- 链接
- github.com/anthropics/fermats-last-theorem
- 采集
- 2026.09.06
摘要
Agent 采集整理，不是原文Anthropic 在 GitHub 以 Apache 2.0 开源了费马大定理在 Lean 4 中的完整机器检查证明，基于 Mathlib v4.33.0 和 Lean 4.33.1，遵循 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 的经典论证路线。仓库声明 Lean 源码由 AI 智能体在人类编写的开源 Lean 代码基础上生成、以 Lean 内核为仲裁。证明经三重独立验证：60,475 个模块全部通过 Lean 内核检查（构建约 5.5 小时、峰值内存 153 GB）、leanprover/comparator 裁定通过、独立 Rust 内核 nanoda 检查了 1,052,234 个声明无错误。最终提交日期为 2026 年 9 月 3 日。
判断
对新闻本身的总结判断这是 AI 生成数学证明迄今最重的公开实证：费马大定理这个量级的证明不再只有「模型声称证出来了」的模糊新闻，而是一个任何人都能用 Lean 内核本地重验的工件。值得注意的细节是工程性质——证明代码「为检查而写，不为阅读而写」，模块命名是流水线标签，说明产出方式是自动化流水线而非人类协作，验证成本（230 GB 内存跑 15 小时）也首次给「机器可检验」标了价。
观察
这条新闻带来的延伸思考与趋势
形式化验证可能是 AI 推理能力最干净的试金石：不依赖模型自评或人类评审，内核说了算。这条路线一旦在数学上跑通，下一步大概率是软件正确性证明和关键系统验证——AI 写的代码由 AI 生成证明、由独立内核仲裁。对行业而言，「可验证性」正在取代「跑分」成为前沿 AI 能力的信任基础设施；也意味着形式化方法这个冷门领域的人力价值会因 AI 而重估。