Would someone be so kind to at least formalize in the notation of metamath the final theorem? I would prefer to double check or modify the proof to the desired form.
In general I think it would be a good idea to mm-formalize each theorem on the "wishlist", more on that later. One formalization ought to be enough, but having a circle of proofs Form1 => Form2 => ... => FormN => Form1 may be welcoming as well. Greetings, L Op dinsdag 21 februari 2023 om 08:37:25 UTC+1 schreef [email protected]: > I'm pretty sure the people who can edit wiki articles is the same as the > set of people with write access to the set.mm repo. > > On Tue, Feb 21, 2023 at 12:02 AM Jim Kingdon <[email protected]> wrote: > >> Oooh, thanks. I've been thinking a bit about formalizing n=3 or n=4 in >> metamath (or perhaps more likely, encouraging others to do so) but I was >> just thinking in terms of something we could accomplish soon, I didn't >> realize that the proof via the Modularity Theorem also needed those cases >> to be proved separately. >> >> I've taken the liberty of writing up what has been posted in this thread >> so far at https://github.com/metamath/set.mm/wiki/Fermat's-Last-Theorem >> which is part of the metamath wiki - I did so with the intention that other >> people could edit as we learn new things (I'm not sure I know the github >> permission system to know who already has an "edit" button but if anyone >> doesn't, just post proposed changes here or to a github issue or whatever). >> On 2/20/23 04:42, David Crisp wrote: >> >> >> (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 >> >> <https://groups.google.com/d/msgid/metamath/308508e3-2ad5-41ae-b362-1c7aa5983207n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> >> -- >> 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/91add638-5d2d-640c-4314-9c104e205916%40panix.com >> >> <https://groups.google.com/d/msgid/metamath/91add638-5d2d-640c-4314-9c104e205916%40panix.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/b9f35272-806e-4bd4-8557-375975e03ea0n%40googlegroups.com.
