fermats-last-theorem

这是一个使用Lean 4形式化验证的费马大定理完整数学证明项目，严格基于Frey–Serre–Ribet–Wiles–Taylor-Wiles证明路径。项目通过Mathlib库构建，所有60,475个模块均经Lean 4.33.1内核逐行检查，仅依赖propext、Classical.choice和Quot.sound三个标准公理，无任何sorr y或非构造性扩展；同时经独立Rust实现的nanoda内核二次验证，确保逻辑可靠性。适用于数学基础研究、形式化方法教学、定理证明工具链验证及可信赖数学知识库建设等场景。