精益 4 中的费马大定理

Fermat's Last Theorem in Lean 4 费马大定理在 Lean 4 上的完整、经过机器检查的证明，构建于 Mathlib（Lean 4.33.1；Mathlib v4.33.0，由 Lakefile.lean 中的提交固定）。这一论点来自弗雷、塞尔、里贝特、怀尔斯和泰勒-怀尔斯。 PROOF-PATH.md 命名了每个步骤以及包含它的精益定理，html/ 文件夹将整个证明显示为可以离线浏览的网页（请参阅下面的“在浏览器中阅读证明”）。研究神器。不维护也不接受贡献。 Theorems/Thm_fermat_last_theorem.lean 声明定理 fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n 和默认构建目标FinalCheck.lean 包含 /-- info: 'fermat_last_theorem' 取决于公理：[propext, Classical.choice, Quot.sound] -/ #print axioms fermat_last_theorem 中的 #guard_msgs 因此构建失败，除非证明完全依赖于 Lean 的三个标准公理（没有抱歉，没有添加公理，没有 native_decide ）。 FinalCheck.lean 还从该定理中派生出 Mathlib 自己的陈述 FermatLastTheorem 。建造。基于 Lean 4.33.1（包括 2026 内核健全性修复）的从头开始构建的 Lake，并从源代码编译了 Mathlib。该存储库的所有 60,475 个模块均已构建，每个声明都经过精益内核检查，公理如上。比较器。 Leanprover/comparator v4.33.0 根据 verify/comparator/Challenge.lean 检查了构建，其中仅使用 Mathlib 陈述了定理。它确认了经过证明的陈述及其提到的每个常量与挑战相同，没有使用其他公理，并且整个证明（包括 Mathlib）通过精益内核重播。结论：你的解决方案没问题！第二个内核。 nanoda 0.4.13，一个用 Rust 编写的独立 Lean 内核，接受相同环境的导出（用 Lean4export 编写）：检查了 1052234 个声明，没有错误。我们用我们自己的四个小补丁（verification/nanoda/patches/）构建了nanoda：一个增加了进度输出，三个加速了其定义等式搜索，如果没有这些补丁，这个证明的一些声明会占用未修改的nanoda几个小时。这些补丁都不会添加、删除或削弱打字规则。没有模块包含 axiom 、抱歉、native_decide、unsafe、extern、implied_by、partial def 或 #eval （Challenge.lean 在设计上使用了抱歉，不是包的一部分）。考虑到对精益内核（或 nanoda）和检查工具的信任，这些检查共同证明上述陈述遵循三个公理。该语句是用 Lean 内置的自然数 + 、 ≤ 、 < 和 ≠ 编写的；它的一个 Mathlib 成分是 ℕ 上的 ^，Mathlib 将其定义为 Lean 的内置求幂，并且比较器检查该语句提到的每个定义是否与普通 Mathlib 的相同。 Mathlib 中的其他内容都不需要信任，因为内核会检查该语句下的所有内容。任何工具都无法检查每个中间定理的含义是否如其名称所暗示的那样；这是供读者判断的，PROOF-PATH.md 命名了每个步骤背后的精益定理，并准确说明了每个命名的经典结果的强度，如此处所证明的。在浏览器中阅读证明 html/ 文件夹（约 390 MB）以静态网页的形式呈现此存储库：逐步证明的路线； 29,511 个定理中的每一个（精确的精益陈述、它引用的内容和引用的内容以及可扩展的依赖图）和 1,450 个定义模块中的每一个（完整的源代码以及哪些语句使用了它）都有一个页面；所有定理和定义名称的搜索框；以图表形式呈现的里程碑定理；以及使用交叉链接呈现的 README.md 、 PROOF-PATH.md 和 ATTRIBUTION.md 。该文件夹是此存储库的一部分，因此克隆或 ZIP 下载已包含它（如果您获得 html/ 作为单独的存档，请将其解压到存储库根目录）。在网络浏览器中打开 html/index.html；一切都可以离线工作，没有网络服务器。这些页面仅在基于 Chromium 的浏览器中进行了机器测试，html/README-DOCS.md 解释了 Lean 文件中引用的内容以及生成的内容（英文摘要和建议参考文献是自动生成的；Lean 声明具有权威性）。您需要 Linux 或 macOS（某些路径对于 Windows 来说太长）、elan（它从 Lean-toolchain 安装 Lean 4.33.1）和网络连接：Lake 从 GitHub 获取 Mathlib 并从源代码编译它，因为没有预构建的 Mathlib 与此工具链匹配（大约 13 分钟，96 个作业）。每个并行作业的构建需要大约 5 GB 内存（一些模块需要高达 36 GB）； .lake/ 下大约有 67 GB 的磁盘空间，加上可以在构建过程中删除的 C 文件（大约 220 GB）。我们的任务耗时 5 小时 32 分钟，执行 96 个作业，内存峰值为 153 GB。比较器大约需要 15 小时（我们的：14 小时 46 分钟），几乎所有时间都在一个内核上重播。我们的峰值内存为 230 GB，因此允许 300 GB。之后运行 nanoda