Post #1735113

I'd like to know which parts of this https://upcommons.upc.edu/server/api/core/bitstreams/905201be-de7e-4a3c-8880-066122168679/content are really finitary and elementary, and which step or steps are the really hard parts. This is a survey of the proof of Mazur's theorem that the p-torsion elements (for p a prime) in E(Q), for a rational elliptic curve E, must have p ≤ 13. This is a *big* hard component for FLT that Kevin @xenaproject Buzzard is deliberately *not* formalising in Lean. I'm listening to a recent talk by Colin McLarty (https://www.youtube.com/watch?v=sEduqKTK4ko) about FLT and the very slow-burning idea that one might be able to prove that it's provable in PA in the technical sense. To my inexpert eyes, Lemma 2.2 in the linked pdf looks like something that could conceiably be reduced to a finitary argument (the only hard part seems to be talking about E[p] as a representation of the absolute Galois group of Q, but that presumably can be reduced to the system of representations of Galois groups of number fields). The other half that, to my understanding, goes to prove the main theorem is Lemma 2.3 and that is immediately serious, with Néron models etc. I know this is ε progress on both big projects, but I think actually isolating the hard kernel theorems is psychologically helpful. I know Kevin is working "mod-1980s", but having a "boss level" (in his terms) that is Lemma 2.3 here (a certain finite extension of the p-th cyclotomic field is unramified) feels more satisfying to me than the monolithic th;df "Mazur's Theorem" (=too hard; didn't formalise).