anthropics/fermats-last-theorem：Lean 4 中机器校验的费马大定理完整证明
来源：GitHub — 2026-09-12 · ⭐ 1,103 · Lean
📋 概述
Anthropic 开源了在 Lean 4 与 Mathlib 中完成的费马大定理完整机器校验证明，论证沿袭 Frey、Serre、Ribet、Wiles 与 Taylor–Wiles 的经典路线。仓库中的 PROOF-PATH.md 逐步标注每个环节对应的 Lean 定理，并附带可离线浏览的网页版证明。它被视为形式化数学的一次标志性展示：困扰人类三百多年的难题，如今每一步都可被机器检验。
🔑 核心要点
- 在 Lean 4 上完成费马大定理的完整机器校验证明，依赖 Mathlib 并锁定版本
- 论证沿用 Frey–Serre–Ribet–Wiles–Taylor 的经典路线，每一步均可追溯
- PROOF-PATH.md 把论证环节与对应 Lean 定理一一对应，便于逐行核验
- 附带离线可浏览的网页版证明，让非 Lean 用户也能通读全貌
💡 金句
当三百多年的数学传奇被拆成一行行可被机器检验的代码，证明的可信度就不再依赖权威，而依赖编译器。
👍 0
👎 0
← 返回 GitHub Trending 首页