费马大定理的 Lean 4 机器检查完整证明开源发布
2026.09.05 · 事件 · 开源项目 · 开源项目
Anthropic 发布费马大定理在 Lean 4 中的完整机器检查证明，基于 Mathlib，并开源。
Anthropic 发布了费马大定理在 Lean 4 中的完整机器检查证明，基于 Mathlib（Lean 4.33.1，Mathlib v4.33.0）。证明采用 Frey、Serre、Ribet、Wiles 和 Taylor-Wiles 的论证，包含 106 个文件 来自帝国理工等项目，并附带 HTML 网页版 供离线浏览。
- 完整机器检查证明，基于 Mathlib
- 论证采用 Frey、Serre、Ribet、Wiles 等
- 提供 HTML 网页版可离线浏览
- 由 AI 代理生成，Lean 作为仲裁者
- Apache 2.0 许可，注明来源归属
为什么值得看
AI 生成并验证数学证明，展示机器检查在数学领域的应用。
适合谁关注
数学研究者、形式化验证开发者、AI 技术爱好者