fermats-last-theorem: Fermat's Last Theorem Fully Verified in Lean 4

This repository fully formalizes Fermat's Last Theorem, a 350-year-old mathematical challenge, in Lean 4. Following the argument path of Frey, Serre, Ribet, Wiles, and Taylor-Wiles, over 60,000 modules have passed the Lean kernel. The final verification stage guarantees that the proof holds using only Lean's three foundational axioms, without 'sorry' or additional axioms.

To enhance verification confidence, two independent tools were used. leanprover/comparator was used to check consistency with standard Mathlib definitions, and nanoda, an independent kernel written in Rust, was used to re-execute the entire environment and prove there were no errors. All declarations are mechanically checked, and the semantics of intermediate steps are documented in PROOF-PATH.md for human review.

An offline web page is provided for visually exploring the proof process. It allows searching through approximately 29,000 theorems and 1,450 definition modules, and tracking the logic behind each step via a dependency graph. Simply open html/index.html without a web server. The Lean source code, generated by AI agents, is optimized for machine verification, prioritizing correctness over readability.

As this is primarily a research artifact, maintenance and contributions are not accepted. It is released under the Apache 2.0 license and is based on the open-source code from the FLT project at Imperial College London and Mathlib. It is useful for developers looking to reference state-of-the-art examples of formal verification or study large-scale integration methods between Lean and Mathlib.