这是一个用 Lean 4 形式化证明费马大定理的研究型仓库，基于 Mathlib，声明并机器检查了自然数版本的费马大定理：当 n ≥ 3 且 a、b、c 为正自然数时，a^n + b^n ≠ c^n。项目包含完整 Lean 源码、最终检查文件、证明路径说明、离线 HTML 浏览文档，以及 comparator 和 nanoda 两套额外验证流程。仓库明确说明该项目是研究产物，不维护且不接受贡献。
适用领域
形式化数学 / 定理证明 / Lean 4 / Mathlib / 数论 / 代数几何与模形式相关形式化 / 数学软件验证 / 机器检查证明 / 科研复现
配置难度
极高。该仓库面向熟悉 Lean 4、Mathlib、形式化数学和高等数论的用户。仅浏览 HTML 文档难度中等，但完整构建和验证需要高性能服务器、长时间运行、丰富的 Lean 工程经验以及对形式化证明工具链的理解。
商业价值
该项目的直接商业落地价值较低，但科研和战略价值很高。它展示了大型数学定理可由 Lean 内核进行端到端机器检查，也体现了 AI 生成或辅助生成形式化证明的潜力。对从事形式化验证、AI for Math、定理证明器、可信软件、科研自动化的团队而言，可作为技术标杆、验证基础设施参考和研究素材；对一般业务系统开发团队，则主要具有品牌、教育和前沿技术观察价值。
01
技术亮点
- 提供费马大定理的 Lean 4 机器检查证明，覆盖经典 Frey-Serre-Ribet-Wiles-Taylor-Wiles 路线。
- 最终定理 fermat_last_theorem 只依赖 Lean 标准三公理：propext、Classical.choice、Quot.sound。
- FinalCheck.lean 使用 #guard_msgs 和 #print axioms 检查证明没有额外 axiom、sorry 或 native_decide。
- README 声称仓库中无 axiom、sorry、native_decide、unsafe、extern、implemented_by、partial def 或 #eval。
- 使用 leanprover/comparator 对挑战文件进行验证，确认声明与 Mathlib 中的挑战定理一致，并重放内核检查。
- 使用独立 Rust Lean 内核 nanoda 进行第二内核验证，提升可信度。
- 包含完整离线 HTML 文档，可搜索定理和定义，并查看依赖图，便于不构建项目时阅读。
- Apache-2.0 许可证，引用和派生来源在 NOTICE 与 ATTRIBUTION.md 中有说明。
- 项目规模极大，是 Lean 4 大型形式化数学工程和 AI 辅助证明生产的重要案例。
02
目标用户
- Lean 4 和 Mathlib 开发者
- 形式化数学研究者
- 数论、代数数论、算术几何方向研究人员
- 对费马大定理形式化证明感兴趣的数学家
- 研究 AI 辅助证明生成的团队
- 定理证明器和内核验证工具开发者
- 高校或研究机构的形式化验证课程/研讨班参与者
03
配置要求
- 操作系统：Linux 或 macOS；Windows 不推荐。
- Lean：Lean 4.33.1，由 lean-toolchain 和 elan 管理。
- Mathlib：v4.33.0，仓库通过 lakefile.lean 固定具体提交。
- 构建工具：Lake。
- 网络：首次构建需要从 GitHub 获取 Mathlib 和相关依赖。
- 基础构建资源：约每个并行 job 需要 5 GB 内存，少数模块可能需要最高约 36 GB。
- 磁盘空间：.lake/ 下约 67 GB；编译产生的 C 文件最多约 220 GB，可在构建过程中删除。
- 参考构建规模：作者环境 96 jobs 下约 5 小时 32 分钟，峰值内存约 153 GB。
- comparator 验证：约 15 小时，主要为单核内核重放；峰值内存约 230 GB，建议预留 300 GB。
- nanoda 验证：需要 bash、git、python3、GNU coreutils、patch、cargo、crates.io 访问；导出环境约 37.8 GB，导出阶段约需 90 GB 内存，检查阶段约需 40 GB。
- HTML 文档：html/ 约 390 MB，Chromium 系浏览器测试通过。
04
适用场景
- 阅读和审查费马大定理在 Lean 4 中的完整形式化证明
- 作为大型 Lean/Mathlib 项目的工程组织、依赖管理和验证流程参考
- 研究 Frey、Serre、Ribet、Wiles、Taylor-Wiles 路线在形式化系统中的表达方式
- 通过 PROOF-PATH.md 对照数学步骤和 Lean 定理
- 使用 html/ 离线浏览 29511 个定理、1450 个定义模块及其依赖图
- 复现 lake build、comparator、nanoda 等多层验证结果
- 评估 AI 生成 Lean 证明代码的可检查性、可读性与工程代价
- 为形式化数学教学、论文讨论或内部技术分享提供案例
05
部署与配置
- 在 Linux 或 macOS 环境中准备系统；不推荐 Windows，因为部分路径过长。
- 安装 elan，用于根据 lean-toolchain 自动安装 Lean 4.33.1。
- 克隆仓库：git clone <repository-url> flt && cd flt
- 确保网络可用，Lake 会从 GitHub 拉取 Mathlib 并从源码编译，因为没有匹配该工具链的预编译 Mathlib。
- 执行构建：LEAN_NUM_THREADS=96 lake build。可根据机器内存降低线程数。
- 构建成功时，输出应包含类似：'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] 和 Build completed successfully。
- 如需运行 comparator 验证，执行：verification/comparator/run.sh，并查看 .verify-work/wrapper/comparator.log 最后一行。
- 如需运行 nanoda 独立内核验证，先运行 comparator 脚本，再执行：verification/nanoda/run.sh，并查看 .verify-work/nanoda/run-*/nanoda.stdout。
- 如只想阅读证明，可直接打开 html/index.html，无需启动 Web 服务，支持离线浏览。
06
风险与注意事项
- 项目明确声明不维护且不接受贡献，后续 Lean/Mathlib 版本升级可能无法直接适配。
- 构建资源需求极高，普通开发者笔记本或 CI 环境很难完整复现。
- 源代码主要面向机器检查而非人类阅读，命名机器生成、注释少，可读性和可审计性较差。
- 证明中间定理的数学含义仍需人工判断；工具只能检查形式系统中的推导有效性，不能保证命名与数学直觉完全一致。
- comparator 和 nanoda 完整验证耗时、耗内存，复现实验门槛很高。
- nanoda 使用了项目方提供的性能补丁，虽然声明不改变类型规则，但仍会增加复现和信任链复杂度。
- 依赖固定版本 Lean 4.33.1 和 Mathlib v4.33.0，对生态版本变动敏感。
- HTML 文档中的英文摘要和参考建议为自动生成，权威内容仍应以 Lean statement 为准。
- 对商业应用直接价值有限，更偏科研、教学和验证基础设施展示。
2026-09-06
第7名
新收录 · github_search
