The landmark theorems and how they depend on each other

The 49 theorems named in PROOF-PATH.md and in the route chapters, with an arrow when one lies below another in the citation graph with no third landmark in between (transitively reduced). Premises are drawn above conclusions, as in the proof. Click a node for its page; every one of the 29,511 theorems has one.

Fermat's Last Theorem proved theorem (every node is proved)arrows run from a premise to the theorem whose proof cites it, possibly through unnamed intermediate theorems

The whole graph is wide and is shown at reading size: scroll sideways, or click it to fit the window; the route pages carry one smaller graph per step.

The landmarks as a table

theorem	step	theorems below	depth	named in
`fermat_last_theorem` Fermat's Last Theorem	The statement	29,488	0	PROOF-PATH.md, README.md, route.md §1
`FreyPackage.fermatLastTheoremFor_of_five_le` Fermat's Last Theorem for prime exponents $p \geq 5$	Reduction to prime exponents p ≥ 5	29,486	2	PROOF-PATH.md
`FreyPackage.no_frey_package` No Frey package exists	The Frey package	29,484	3	PROOF-PATH.md, route.md §1
`FreyPackage.of_counterexample` Frey package from a counterexample of exponent $p \geq 5$	The Frey package	0	3	PROOF-PATH.md, route.md §1, route.md §2
`FreyPackage.Mazur_Frey` Irreducibility of the mod- $p$ torsion module of the Frey curve	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	5,435	4	PROOF-PATH.md, route.md §2
`FreyPackage.frey_isModular` Modularity of the Frey curve	Modularity (Wiles, Taylor–Wiles)	27,797	4	PROOF-PATH.md, route.md §2
`FreyPackage.level_lowering_to_two` Level lowering to $Γ_{0} (2)$ for the Frey curve	Level lowering (Ribet)	27,851	4	PROOF-PATH.md, route.md §2
`ModularForm.S2_Gamma0_2_eq_zero` Vanishing of weight- $2$ cusp forms of level $2$	No weight-2 cusp forms of level 2	0	4	PROOF-PATH.md, route.md §2, route.md §5
`FreyPackage.Mazur_Frey_of_a_mod_eight` Irreducibility of $E_{P} [p]$ when $a \equiv 3 (mod 8)$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	104	5	PROOF-PATH.md, route.md §3
`FreyPackage.frey_no_cofixed_eleven` No Galois-stable cofixed line at $p = 11$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	3	5	PROOF-PATH.md, route.md §3
`FreyPackage.frey_no_cofixed_large` Mazur at $p \geq 17$ : no cofixed line	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	5,377	5	PROOF-PATH.md, route.md §3
`FreyPackage.frey_no_cofixed_small` No Galois-stable cofixed line for $p \in {5, 7, 13}$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	6	5	PROOF-PATH.md, route.md §3
`FreyPackage.frey_reducible_hasCofixedLine` Reducible Frey representation yields a Galois-stable cofixed line	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	82	5	PROOF-PATH.md, route.md §3
`FreyPackage.level_lowering_to_two_of_conductorLevel` Level lowering for the Frey curve down to $Γ_{0} (2)$	Level lowering (Ribet)	12,980	5	PROOF-PATH.md, route.md §5
`FreyPackage.modularRepOfConductorLevel` Conductor-level modularity of the Frey curve's mod- $p$ representation	Level lowering (Ribet)	27,798	5	PROOF-PATH.md
`WeierstrassCurve.modularity_of_semistableModel` Modularity of semistable integral Weierstrass models	Modularity (Wiles, Taylor–Wiles)	27,796	5	PROOF-PATH.md
`FreyPackage.freyGaloisRep_isUnramifiedAt` Frey $p$ -torsion is unramified outside ${2, p}$	Level lowering (Ribet)	42	6	route.md §5
`FreyPackage.level_lowering_at_p_of_conductorLevel` Mazur–Ribet level lowering at $p$ for conductor levels	Level lowering (Ribet)	6,090	6	PROOF-PATH.md, route.md §5
`FreyPackage.level_lowering_odd_prime_of_conductorLevel` Ribet level lowering at an odd prime $q \neq = p$	Level lowering (Ribet)	12,496	6	PROOF-PATH.md, route.md §5
`ModularForm.S2_Gamma0_one_eq_zero` Weight-two cusp forms of level one vanish	No weight-2 cusp forms of level 2	0	6	PROOF-PATH.md, route.md §5, route.md §6
`WeierstrassCurve.isResiduallyModularOfLevel_of_switch` Mod- $5$ transport of residual modularity across the $3$ – $5$ switch	Modularity (Wiles, Taylor–Wiles)	0	6	PROOF-PATH.md, route.md §4
`WeierstrassCurve.isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel` Residual modularity mod $3$ at a cube-free level, with inertia condition	Modularity (Wiles, Taylor–Wiles)	7,306	6	PROOF-PATH.md, route.md §4
`WeierstrassCurve.mazurStepThree_not_inZeroComponentAt` Mazur's Step 3 at one multiplicative prime $ℓ$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	5,253	6	PROOF-PATH.md, route.md §3
`WeierstrassCurve.modThreeOrFiveIrreducible` One of $ρ ˉ_{W, 3}$ , $ρ ˉ_{W, 5}$ is irreducible	Modularity (Wiles, Taylor–Wiles)	25	6	PROOF-PATH.md, route.md §4
`WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_inertia_moves_torsion_of_eq_three_of_not_cube_dvd` Modularity lifting at $p = 3$ from a prescribed residual level	Modularity (Wiles, Taylor–Wiles)	23,032	6	PROOF-PATH.md, route.md §4
`WeierstrassCurve.modularityLiftingAtConductor_threeFive_of_level_of_not_sq_dvd_of_not_cube_dvd` Modularity lifting at $p \in {3, 5}$ for $p^{2} ∤ M_{0}$	Modularity (Wiles, Taylor–Wiles)	22,708	6	PROOF-PATH.md, route.md §4
`WeierstrassCurve.threeFiveSwitchCurve` The 3–5 switch for semistable integral models	Modularity (Wiles, Taylor–Wiles)	124	6	PROOF-PATH.md, route.md §4
`fermatLastTheoremFive` Fermat's Last Theorem for the exponent $5$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	0	6	PROOF-PATH.md, route.md §3
`fermatLastTheoremSeven` Fermat's Last Theorem for exponent $7$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	2	6	PROOF-PATH.md, route.md §3
`CuspForm.newformBadPrimeCoeff` Bad-prime coefficients of weight- $2$ newforms on $Γ_{0} (N)$	Level lowering (Ribet)	68	7	route.md §5
`FreyCurve.isPeuRamifieeAt_odd_of_integralForm` Frey curve is peu ramifiée at every odd prime	Level lowering (Ribet)	4	7	PROOF-PATH.md, route.md §5
`FreyPackage.eigenformResidualAttachmentAtFamily` Eichler–Shimura residual attachment at every level	Level lowering (Ribet)	1,297	7	route.md §5
`GaloisRep.DeformationRingData.exists_surjective_algHom_of_heckeGaloisRepDatum` Existence of a surjection $R ↠ T$	Modularity (Wiles, Taylor–Wiles)	6	7	PROOF-PATH.md, route.md §4
`IsCyclotomicExtension.Rat.seven_pid` The ring of integers of $Q (ζ_{7})$ is principal	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	0	7	PROOF-PATH.md, route.md §3
`ModularCurve.eisensteinQuotientInvariantsFiniteAt_heckeModuleBar` Finiteness of the Galois invariants of the Eisenstein quotient of $J_{0} (p)$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	5,128	7	route.md §3
`ModularCurve.mazurQuotientSpecialization_heckeModuleBar` Specialisation of the Eisenstein quotient away from $p$	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	2,179	7	route.md §3
`ResidualGaloisRep.isAbsolutelyIrreducible_of_isIrreducible_of_isOdd` Odd irreducible residual representations are absolutely irreducible	Modularity (Wiles, Taylor–Wiles)	0	7	PROOF-PATH.md, route.md §7
`WeierstrassCurve.fifteenIsogenyClassification` Four possible $c_{4}^{3} /Δ$ for rational $15$ -isogenies	Modularity (Wiles, Taylor–Wiles)	24	7	PROOF-PATH.md, route.md §4
`WeierstrassCurve.isModularModelOfLevel_conductorLevel_of_not_cube_dvd_of_modRepIsIrreducible_of_not_sq_dvd` Descent to the conductor level when $p^{2} ∤ N$	Modularity (Wiles, Taylor–Wiles)	11,044	7	route.md §4
`WeierstrassCurve.isModularModelOfLevel_of_patchingDatum` From a patching datum to modularity at an explicit level	Modularity (Wiles, Taylor–Wiles)	64	7	route.md §4
`WeierstrassCurve.isResiduallyModularOfLevel_div_of_isUnramifiedAt_sqf` Level lowering at an unramified prime exactly dividing the level	Level lowering (Ribet)	12,481	7	route.md §5
`WeierstrassCurve.nonempty_deformationRingData_ordinaryCondition_of_isSemistableModel` Representability of the ordinary deformation problem for a semistable curve	Modularity (Wiles, Taylor–Wiles)	169	7	route.md §4
`WeierstrassCurve.threeFiveAuxiliaryCurveExists` Auxiliary curve for the 3–5 switch	Modularity (Wiles, Taylor–Wiles)	77	7	route.md §4
`flt_regular` Kummer's theorem: Fermat's Last Theorem for regular primes	Irreducibility (Mazur; exponents 5, 7, 11, 13 settled directly)	0	7	PROOF-PATH.md
`Algebra.PatchingDatum.nonempty_patchingLevel_bot` Taylor–Wiles patching: a patched level with zero relation ideal	Modularity (Wiles, Taylor–Wiles)	5	8	route.md §4
`WeierstrassCurve.exists_forall_not_isRoot_Psi3_specialization` Specialisations with rootless $3$ -division polynomial in a weighted family	Modularity (Wiles, Taylor–Wiles)	5	8	route.md §4
`WeierstrassCurve.galoisRepIsIrreducible_three_of_forall_eval_Psi3_ne_zero` Mod-3 irreducibility from $Ψ_{3}$ with no rational root	Modularity (Wiles, Taylor–Wiles)	3	8	route.md §4
`LanglandsTunnell.exists_isWeightOneChiNegThreeRealized_eq_trace_lift` Weight-one form attached to a surjective mod-3 representation	Modularity (Wiles, Taylor–Wiles)	6,804	9	PROOF-PATH.md, route.md §4
`AutomorphicForm.exists_weightOne_cuspForm_of_isCusp_viaCompactCuspNotion` From cuspidal adelic eigensystems to classical weight-one cusp forms	Modularity (Wiles, Taylor–Wiles)	6	10	route.md §4