Fermat's Last Theorem in Lean 4

The proof of Fermat’s Last Theorem has been fully formalized in Lean 4 (v4.33.1) using Mathlib v4.33.0, showing an + bn ≠ cn for every n ≥ 3 with positive a, b, c, based solely on Lean’s three core axioms. The repository compiles 60,475 modules, verifies with both the official Lean kernel and the Rust-based nanoda kernel, and includes an offline HTML browser of the proof hierarchy.