人类数学史上最难定理的“零错误”机器验证：费马大定理在 Lean 4 中完整形式化证明

这不是一个“求解”费马大定理的工具，而是一份经受住三重独立核验、逐行由数学引擎严格检查的「终极证明文档」——它用现代形式化证明语言 Lean 4，将怀尔斯（Wiles）1995年震惊世界的证明，从纸面演算彻底翻译为计算机可验证的逻辑链条。全证明无任何未证假设（sorry）、不引入额外公理，仅依赖 Lean 内置的三个标准经典公理，真正实现了“人类直觉→机器可读→机器可验”的闭环。

核心功能

提供费马大定理的首个完整、开源、可离线浏览的形式化证明库：所有60,475个Lean模块全部通过编译，包含29,511个已验证定理和1,450个定义模块，不再是论文附录或片段代码，而是可直接克隆、构建、审查的完整工程。
支持零依赖本地浏览器阅读整套证明：项目自带约390MB的html/静态站点，打开html/index.html即可离线浏览每一步推导——点击任一引理查看其精确Lean声明、所有引用来源、被引用位置，甚至展开交互式依赖图，让抽象证明变得“可导航、可追溯”。
内置多层级交叉验证机制，杜绝“幻觉证明”风险：不仅通过Lean官方内核（v4.33.1）全程检查，还使用独立Rust实现的nanoda内核二次验证，并借助leanprover/comparator比对Mathlib标准陈述，确保所证命题与数学界公认表述完全一致、无定义漂移。
精准标注每步证明对应的数学里程碑：通过PROOF-PATH.md文件，将Frey曲线构造、Serre模性猜想、Ribet定理、Wiles-Taylor模性提升等关键环节，一一映射到具体Lean定理名（如modularity_of_semistable_elliptic_curves），让数学家能快速定位并复核核心段落。
严格控制公理边界，明确声明可信基底：默认构建脚本FinalCheck.lean强制校验最终定理仅依赖propext（命题外延性）、Classical.choice（选择公理）和Quot.sound（商类型健全性）三项，拒绝任何隐藏假设，为后续元数学分析提供清晰基础。
全代码库无危险语法，保障可审计性：扫描确认不含axiom、unsafe、extern、partial def等高风险构造，连#eval（运行时求值）都被禁用，确保整个证明栈纯粹基于逻辑推导，而非黑盒计算。
提供Mathlib兼容接口，无缝对接主流形式化生态：最终导出Mathlib标准命名的FermatLastTheorem，且comparator验证其定义与Mathlib v4.33.0完全一致，开发者可直接在自己的Mathlib项目中import FermatLastTheorem进行引用或延伸。

技术亮点

双内核验证架构：除Lean官方4.33.1内核外，项目专门适配了独立实现的nanoda（Rust编写）内核，并为其贡献了4处必要补丁（含进度提示与性能优化），实现“同一证明、两套引擎、零差异输出”，极大降低单一内核缺陷导致误判的风险。
Mathlib深度绑定与版本锁定：明确指定Mathlib v4.33.0（对应commit哈希固化于lakefile.lean），避免因上游库更新引发的隐式行为变更，保证构建结果可重现——这是大型形式化项目长期可维护的关键设计。
声明式构建约束驱动验证流程：不依赖人工测试脚本，而是通过#guard_msgs指令在Lean中直接断言公理集，使验证成为类型检查的一部分；构建失败即意味着证明存在漏洞，将形式验证真正融入CI范式。
面向人类可读的证明导航系统：html/生成器并非简单文档化，而是构建了完整的知识图谱：每个定理页显示“谁引用我/我引用谁”，搜索框覆盖全部29,511个定理名，关键里程碑以图谱形式可视化连接，让非Lean专家也能把握证明宏观结构。

适合哪些人用

本项目主要面向三类用户：

数学研究者与逻辑学家：可将此作为模性定理、伽罗瓦表示、椭圆曲线等方向的形式化参考基准。例如，某高校数论课题组正基于此库中的semistable_elliptic_curve_modularity模块，快速搭建新猜想的验证框架，省去从头形式化基础定理的时间。

形式化验证教育者：课程中可直接展示html/index.html，让学生点击进入“Frey曲线不可模性”证明页，观察如何将代数几何直觉转化为¬ (∃ (E : EllipticCurve ℤ), is_semistable E ∧ is_modular E)这样的精确命题，直观理解形式化鸿沟如何被跨越。

编程语言与定理证明工具开发者：项目是Lean 4大规模工程实践的标杆案例，其Lake构建配置、跨内核验证流程、HTML文档生成策略，均为同类工具链开发提供了经过实战检验的设计模式。

快速上手

无需安装复杂环境即可体验核心价值：

访问GitHub页面，点击绿色Code按钮 → Download ZIP，解压后进入目录
直接双击打开html/index.html（推荐Chrome/Edge），无需服务器，离线浏览全部证明
在搜索框输入fermat_last_theorem，直达主定理页，点击“Cited by”查看其如何被FinalCheck.lean调用
如需构建验证：确保已安装elan和lake（Lean 4.33.1），执行lake build FinalCheck，成功即代表本地环境通过全部检查

同类对比 / 注意事项

目前全球尚无其他项目完成费马大定理的端到端形式化证明。此前Coq中曾有部分工作（如FLT-regular仅处理正则素数情形），但本项目是首个覆盖全部n≥3的完整证明。需特别注意：

非活跃维护项目：README明确声明“Not maintained and not accepting contributions”，它是一个冻结的研究快照，而非持续演进的软件产品，适合学习与引用，但不宜作为长期依赖的基础库。
硬件要求较高：HTML文档包达390MB，完整构建需约16GB内存与数小时编译时间，普通笔记本建议优先使用预生成HTML版。
不替代数学理解：工具无法自动判断某个中间引理的命名是否准确反映其数学强度（如“weak Serre conjecture”在此证明中实际采用何种版本），这仍需人类专家结合PROOF-PATH.md审阅。