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/1ceff94e-aa1a-411f-bb69-8dea80fd6a59n%40googlegroups.com. -- 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/8F1764D0-2354-465D-ABF6-A15C7A8B9BDE%40panix.com.
