(Breaking my years-long lurking habit to post this :)) One thing that's often left out in discussions of how to formalize FLT is that even if the entire Frey - Serre - Ribet - Wiles sequence is included, the cases n=3 and n=4 will still need to be added as separate proofs. It's not obvious from a 'casual' read of Wiles' paper, but the level-lowering procedure used by Serre and Ribet to establish the non-modularity of the Frey curve is only guaranteed to work if the exponent in the Fermat equation is an odd prime != 3. Induction over the multiplicative structure of N then establishes the theorem for all n except those whose only prime factors are 2 and 3, but the n=3 and n=4 cases would still need to be proved separately to complete the proof.
Luckily these two cases are fairly elementary to prove individually (especially compared to the monumental task of formalizing the entire modularity theorem) and so are often handwaved away in informal discussions, but a formal system like Metamath obviously can't do that. Dave On Sunday, 19 February 2023 at 04:05:37 UTC [email protected] wrote: > Looks like http://www.ipam.ucla.edu/abstract/?tid=19347&pcode=MAP2023 has > both an abstract (which goes into more detail about what the talk is about) > and a video of the talk. > > Maybe you'd be able to figure out where this fits into your outline; I'm > afraid I'm even less far up the learning curve than you. > > > On February 18, 2023 7:58:11 PM MST, Steven Nguyen <[email protected]> > wrote: >> >> I've actually taken some notes over Fermat's Last Theorem: >> https://docs.google.com/document/d/19dXkojJJt6gq9rYLo6zbz7HpHpD9iMJJkY0LEpGqPs0/edit?usp=sharing >> Although so far, all that has come out of it are some useful resources, >> definitions, and the overall structure of Fermat's Last Theorem, which I >> summarize here: >> >> 1. >> >> Modularity Theorem (previously the Taniyama-Shigura(-Weil) >> conjecture): every rational elliptic curve is modular >> 2. >> >> Yves Hellegouarch came up with the idea of associating hypothetical >> solutions (a, b, c) with elliptic curves of the form y^2 = x(x − >> a^n)(x + b^n). >> 1. >> >> Such curves are called Frey curves or Frey-Hellegouarch curves. >> 3. >> >> Ribet’s Theorem (previously called the epsilon or ε-conjecture): All >> Frey curves are not modular >> >> Note that the final paper by Wiles proved a special case of the >> modularity theorem for semistable curves over ℚ. In this case, "Frey curves >> are semistable" would have to be proved as well. >> >> This is enough to prove FLT. If there were any solutions, then there >> would be a corresponding Frey curve. By Ribet’s Theorem, the curve would >> not be modular, but that contradicts the Modularity Theorem. Therefore >> there are no fermat triples, FLT is proved. ∎ >> >> >> However, I admit I don't understand almost all of the theory behind >> FLT... I've never heard of local field class theory. So that's quite an >> interesting link. >> On Thursday, February 16, 2023 at 8:36:10 PM UTC-6 [email protected] >> wrote: >> >>> I know this is a bit of a white whale and there is a lot of mathematics >>> to formalize before this is even in reach. But when the formal math >>> community (taken as a whole) is at 99 out of 100 of the Top 100 list, of >>> course it is easy to focus on the one. >>> >>> Anyway the news is that there was a recent talk on formalizing local >>> field class theory which apparently is one of the things that will be >>> needed. https://mathstodon.xyz/@tao/109877480759530521 >>> >> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/308508e3-2ad5-41ae-b362-1c7aa5983207n%40googlegroups.com.
