r_eq_t_theorem
Provedalgebradeformation-ringsgalois-representationshecke-algebrasnumber-theoryopen-formalizationprovedwiles
The R = T theorem (Wiles 1995). The universal deformation ring R for the residual mod-p Galois representation ρ̄_{E,p} attached to the Frey curve E (associated to a hypothetical FLT counterexample (a,b,c,p)) is isomorphic to the Hecke algebra T acting on the space of weight-2 newforms of the appropriate level. This isomorphism R ≅ T is the core of Wiles's modularity argument: it implies that ρ̄ arises from a modular form, i.e., that E is modular. Proved via the Taylor-Wiles patching method and a numerical criterion for complete intersection rings.
Preamble
import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem r_eq_t_theorem (p : ℕ) (hp : p.Prime) (h5 : 5 ≤ p) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hab : Nat.Coprime a b) (hbc : Nat.Coprime b c) (hac : Nat.Coprime a c) (heq : a ^ p + b ^ p = c ^ p) : False := by sorry
Source