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 <king...@panix.com> 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 kin...@panix.com 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 <icecream...@gmail.com> >> 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 kin...@panix.com >>> 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu5ucCfyJtMX0-zCrY6dsGV9nx9ebs3p0XL2-cfB6po7A%40mail.gmail.com.
