Fermat's Last Theorem
Proof Structure · Knowledge Graph · Python Verification
NOTE: Deep theorems (Serre conjecture, Ribet level lowering, Wiles R=T) are marked as stubs.
Their proofs are at the Fields Medal level and are the subject of the Imperial College FLT formalization
project (EPSRC 2024-2029, Kevin Buzzard).
Ch 1
Introduction & Historical Background
FLT Proof
Fermat's 1637 marginal note, the 358-year journey, and the structure of Wiles' proof.
Lean: ch06_serre_ribet_wiles.lean
Verification:- PASS FLT n=3 brute-force: no solutions (1 <= x <= y <= 100)
- PASS FLT n=4 brute-force: no solutions (1 <= x <= y <= 50)
- PASS FLT n=5 brute-force: no solutions (1 <= x <= y <= 30)
Ch 2
The Frey Curve Construction
Elliptic CurvesFLT Proof
Assuming a^p + b^p = c^p, construct E: y^2 = x(x - a^p)(x + b^p). Key properties: non-singular, semistable, conductor N_E = 2.rad(abc).
Lean: ch02_frey_curve.lean
Verification:- PASS Frey(1,2,3): discriminant = 82944 != 0
- PASS Frey(3,5,3): discriminant != 0
- PASS Frey(1,2,5): discriminant != 0
- PASS N_E squarefree: all Tate exponents in {0,1}
Ch 3
Elliptic Curves (Background)
Elliptic Curves
Weierstrass equations, discriminant Delta, j-invariant, group law, Mordell's theorem, torsion subgroups.
Lean: ch01_elliptic_curve.lean
Theorems:theorem_7_1theorem_7_2theorem_7_3
Verification:- PASS Group law 10/10 tests (identity, inverse, commutativity, associativity)
- PASS Point counting: 11 primes, all satisfy Hasse bound
- PASS E[2] is isomorphic to Z/2Z x Z/2Z (Klein four-group)
Ch 4
Modular Forms
Modular FormsComplex Analysis
Holomorphic functions on the upper half-plane, Eisenstein series E_4, E_6, cusp forms, q-expansions, Hecke operators T_p.
Lean: ch03_modular_curves.lean
Verification:- PASS E_6(i) = 0 (by symmetry)
- PASS M_*(SL_2(Z)) = C[E_4, E_6] dimension check
- PASS S_2(Gamma_0(2)) = 0 (genus formula: g_0(2) = 0) -- CRITICAL
- PASS T_2 E_4 = 9E_4 (Hecke eigenvalue 1+2^3=9)
- PASS T_2 Delta = tau(2)Delta = -24Delta (Ramanujan tau)
- PASS Hecke multiplicativity: T_2 T_3 = T_6
Ch 5
Hecke Operators and the Hecke Algebra
Modular Forms
The Hecke algebra T generated by T_p acting on S_2(Gamma_0(N)). The Eichler-Shimura relation connects T_p to Frobenius on J_0(N).
Lean: ch03_modular_curves.lean
Verification:- PASS T_p action on q-expansion implemented
- PASS Eigenvalue property verified on Delta
Ch 6
Galois Representations
Galois ReprAbstract Algebra
The absolute Galois group G_Q, l-adic representations, the mod p representation rho_{E,p} attached to an elliptic curve.
Lean: ch04_galois.lean
Verification:- PASS E[2] Galois action: Q(E[2]) = Q, trivial representation
- PASS rho_{E,2} image = {identity} subset GL_2(F_2)
Ch 7
Deformation Theory and R = T
Galois Repr
The universal deformation ring R of rho-bar, the Hecke algebra T acting on S_2(Gamma_0(N)), Taylor-Wiles patching to prove R = T.
Lean: ch05_deformation.lean
Verification:- STUB Deep theorem: not verifiable by elementary methods
Ch 8
Serre's Conjecture
Galois ReprModular Forms
Every odd, absolutely irreducible mod l representation of G_Q is modular (Khare-Wintenberger 2008).
Lean: ch06_serre_ribet_wiles.lean
Verification:- STUB Deep theorem: proof >100 pages, stub only
Ch 9
Ribet's Level Lowering
FLT Proof
If rho-bar arises from S_2(Gamma_0(N)) and is unramified at p|N, then rho-bar arises from S_2(Gamma_0(N/p)).
Lean: ch06_serre_ribet_wiles.lean
Verification:- STUB Deep theorem: Ribet 1990, stub only
Ch 10
Modularity Lifting
FLT Proof
If rho-bar is modular, then any 'nice' lift rho is also modular. Wiles & Taylor-Wiles 1995.
Lean: ch06_serre_ribet_wiles.lean
Verification:- STUB Deep theorem: ~100 pages, stub only
Ch 11
The FLT Contradiction
FLT Proof
Assemble the chain: Frey curve -> modularity -> Ribet level lowering -> S_2(Gamma_0(2)) = 0 -> contradiction.
Lean: ch06_serre_ribet_wiles.lean
Verification:- PASS dim S_2(Gamma_0(2)) = 0 (elementary genus formula)
- PASS Full proof chain numerically consistent
Ch A
Appendix: n = 4 (Infinite Descent)
Abstract Algebra
Fermat's own proof: x^4 + y^4 = z^4 has no non-trivial integer solutions by infinite descent.
Lean: flt_base_cases.lean
Verification:- PASS Brute force no solutions for x,y <= 50
Ch B
Appendix: n = 3 (Eisenstein Descent)
Abstract AlgebraComplex Analysis
Euler's proof using Z[omega] where omega = e^{2pi i/3}. Eisenstein integers, lambda = 1 - omega, lambda-adic descent.
Lean: flt_base_cases.lean
Verification:- PASS Z[omega] arithmetic: omega^3 = 1, omega^2+omega+1=0
- PASS lambda = 1-omega, N(lambda)=3, prime in Z[omega]
- PASS Lemma 12.6: alpha = 0, +/-1 (mod lambda) for all Z[omega] elements
- PASS Lemma 12.7: lambda does not divide alpha -> alpha^3 = +/-1 (mod lambda^4): 294/294
- PASS 3 = (-omega^2)lambda^2 (associate)
- PASS Factorization: x^3 + y^3 = (x+y)(x+omega y)(x+omega^2 y)
- PASS Lemma 12.9: lambda divides one of x,y,z in x^3+y^3+z^3=0
Learning Path
5 phases, from abstract algebra to the FLT contradiction:
Phase 2: Elliptic Curves: Weierstrass, Mordell theorem, Frey curve
67 concepts
- frey
- elliptic curve
- conductor
- semistable
- uniformisation
- weierstrass
- j-invariant
- singular
- mordell
- discriminant
- frey curve
- reduction
- bad reduction
- good reduction
- point at infinity
- torsion
- rational point
- lattice
- proposition_7_1
- theorem_7_1
- theorem_7_2
- lemma_7_3
- proposition_7_2
- proposition_7_3
- proposition_7_4
- lemma_7_4
- proposition_7_5
- corollary_7_1
- theorem_7_3
- proposition_7_6
- theorem_9_4
- theorem_9_2
- theorem_14_2
- theorem_13_1
- proposition_13_1
- lemma_3_1
- thm_proposition_3_1
- thm_proposition_3_2
- thm_theorem_3_2
- thm_proposition_3_3
- thm_theorem_7_2
- good_reduction
- bad_reduction
- multiplicative_reduction
- additive_reduction
- node_singularity
- cusp_singularity
- cayley_bacharach
- point_at_infinity
- singular_point
- pp_group_scheme
- torsion_points
- point_at_infinity_o
- elliptic_curve_group_law
- p-division_points_e[p]
- ℓ-adic_tate_module
- ℓ-adic_integers_z_ℓ
- inverse_limit
- inverse_system
- lattice_l
- uniformisation_theorem
- e[n]_≅_z_nz⊕z_nz
- two-dimensional_f_l_vector_space
- tate_ℓe_≅_z_ℓ_⊕_z_ℓ
- semistable_elliptic_curve
- conductor_n_e_general
- cayley-bacharach_theorem
Phase 4: Galois Repr: ℓ-adic, deformation theory, R=T
71 concepts
- galois representation
- absolute galois
- unramified
- dirichlet
- l-adic
- tate module
- functional equation
- theorem_11_1
- proposition_11_1
- proposition_11_2
- proposition_11_3
- theorem_11_2
- lemma_11_2
- lemma_11_3
- lemma_11_4
- lemma_11_5
- lemma_11_6
- lemma_11_7
- lemma_5_3
- proposition_11_4
- proposition_11_5
- proposition_11_6
- theorem_11_3
- proposition_11_7
- lemma_11_8
- lemma_11_9
- lemma_11_10
- corollary_11_1
- theorem_11_11
- lemma_11_12
- theorem_11_13
- theorem_11_4
- deformation_ring
- minimal_deformation_ring
- taylor_wiles_method
- R_equals_T
- kisin_RT_machinery
- crystalline_representation
- semistable_representation
- minimal_p_adic_lift
- compatible_system
- kill_ramification
- frobenius_element
- hodge_tate_weight
- p_adic_lift
- degruyter_compatible_system
- hecke_l_function
- absolute_galois_group_g_q
- krull_topology
- galois_representation_ρ:_g_q→gl_nr
- mod_ℓ_galois_representation
- ℓ-adic_galois_representation
- cyclotomic_character_χ
- p-adic_cyclotomic_character
- odd_galois_representation
- serres_modularity_conjecture
- galois_action_on_torsion_points
- ρ_e,ℓ:_elliptic_curve_galois_representation
- modular_galois_representation
- conductor_n_serre
- weight_k_serre
- nebentypus_ε
- unramified_at_prime_p
- trace_of_frobenius_trfrob_p,ρ
- frobenius_element_in_g_q
- decomposition_group_d_p
- inertia_group_i_p
- ribets_level_lowering
- langlands-tunnell_theorem
- 3-5_trick_wiles
- frey_curve_galois_representation
Phase 5: FLT Proof: Ribet, Wiles, contradiction
88 concepts
- serre
- modularity
- ribet
- wiles
- taylor
- taniyama
- shimura
- contradiction
- epsilon conjecture
- theorem_3_1
- proposition_3_1
- proposition_3_2
- corollary_1_2
- theorem_3_2
- theorem_12_1
- theorem_12_2
- lemma_12_2
- lemma_12_3
- lemma_12_4
- lemma_12_5
- lemma_12_6
- lemma_12_7
- lemma_12_8
- lemma_12_9
- lemma_12_10
- lemma_12_11
- lemma_8_7
- theorem_12_12
- thm_theorem_3_1
- thm_proposition_7_1
- thm_theorem_7_1
- thm_theorem_8_1
- thm_corollary_8_1
- thm_theorem_8_3
- thm_theorem_8_4
- thm_theorem_8_5
- thm_theorem_8_6
- thm_theorem_8_7
- thm_theorem_8_8
- thm_theorem_8_9
- thm_theorem_8_10
- thm_theorem_8_11
- thm_lemma_9_1
- thm_lemma_9_2
- thm_proposition_9_2
- thm_theorem_9_1
- thm_lemma_9_3
- thm_proposition_9_3
- thm_theorem_9_4
- thm_lemma_9_7
- thm_lemma_9_10
- thm_lemma_9_13
- thm_lemma_9_14
- thm_proposition_11_3
- thm_lemma_11_3
- thm_lemma_11_5
- thm_lemma_11_6
- thm_proposition_11_4
- thm_proposition_11_5
- thm_theorem_11_3
- thm_lemma_11_8
- thm_corollary_11_1
- thm_theorem_12_1
- thm_theorem_12_2
- thm_lemma_12_2
- thm_lemma_12_3
- thm_lemma_12_4
- thm_lemma_12_5
- thm_lemma_12_6
- thm_lemma_12_7
- thm_lemma_12_8
- thm_lemma_12_9
- thm_lemma_12_10
- thm_lemma_12_11
- thm_theorem_12_12
- thm_proposition_13_1
- thm_theorem_14_2
- thm_proposition_14_3
- thm_theorem_14_4
- thm_corollary_14_1
- thm_theorem_14_1
- thm_lemma_14_5
- thm_lemma_14_6
- pythagorean_triple
- abc_conjecture
- induction_on_primes
- serre_conjecture
- level_one_serre
Lean 4 Source Files
- ch01_elliptic_curve.lean - Elliptic curve definitions
- ch02_frey_curve.lean - Frey curve construction
- ch03_modular_curves.lean - Modular forms, Hecke, S_2(Gamma_0(2))=0
- ch04_galois.lean - Galois representations
- ch05_deformation.lean - Deformation rings, R=T
- ch06_serre_ribet_wiles.lean - Serre, Ribet, Wiles, FLT assembly
- flt_base_cases.lean - n=3, n=4 wrappers