Fermat's Last Theorem (Imperial)
The blueprint of Fermat's Last Theorem (Imperial), read at commit a3210204 (2026-10-22): one article for each of its 172 nodes whose Lean declarations it names and marks formalized, or in Mathlib. Its other 69 nodes have no article, and a section of only those is left out: the map records what the project contains, not what it plans. A statement for which the blueprint marks no proof \leanok says so. Dependencies are the blueprint's \uses: a statement's under Depends on, a proof's under Proof depends on.
The text is the blueprint's, under its Apache-2.0 license: each page has a section's prose, remarks and examples in the blueprint's order, with each node's statement and proof where the node stands.
- Introduction
- First reductions of the problem
- Reducibility of p-torsion of the Frey curve
- An example of an automorphic form
- Automorphic forms and the Langlands Conjectures
- Miniproject: Frobenius elements
- Miniproject: Adeles
- Miniproject: Haar Characters
- Miniproject: Fujisaki's Lemma
- Miniproject: Quaternion algebras
- Miniproject: Hecke Operators
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.