费马大定理的 Lean 4 机器可校验证明仓库开放
来源：github.com — github.com · 138 分 · by aaraujo002
📋 概述
Anthropic 在 GitHub 开放 fermats-last-theorem 仓库，其中包含费马大定理（FLT）的完整机器可校验证明源码：约 1450 个定义模块、2.95 万个命题模块与 2.95 万个证明模块，全经 Lean 4.33.1 与 Mathlib v4.33.0 编译通过，并经受 comparator 与独立内核实现 nanoda 的双重校验。仓库附静态网页与可复现脚本。
🔑 核心要点
- 仓库包含完整的机器校验证明。
- 含 1450 个定义、2.95 万命题与证明模块。
- 经 Lean 内核与独立实现 nanoda双重验证。
- 依赖公理仅 propext、Classical.choice、Quot.sound。
- 附静态 HTML 页面与可复现脚本。
💡 金句
当名字与命题不一致时，以命题为准——那才是真正被证明的东西。
👍 0
👎 0
← 返回 Hacker News 首页