A complete, machine-checked proof of Fermat's Last Theorem in Lean 4, built on Mathlib (Lean 4.33.1; Mathlib v4.33.0). The argument follows Frey, Serre, Ribet, Wiles and Taylor-Wiles. The repository includes PROOF-PATH.md and an html folder for browsing.

This research artifact is not maintained and not accepting contributions. The theorem states that for natural numbers n ≥ 3 and positive a, b, c, a^n + b^n ≠ c^n. The build verifies that the proof rests only on Lean's three standard axioms, with no sorry or added axioms.

Verification included a from-scratch lake build, a comparator check against the challenge, and an independent Rust kernel (nanoda) that checked 1,052,234 declarations. The comparator confirmed the statement matches the challenge and uses only Mathlib definitions.

The html folder (about 390 MB) presents the proof as static web pages, with 29,511 theorems and 1,450 definition modules, searchable and browsable offline.