It's commented out, but you can search set.mm for "Fermat's Last Theorem"
and it's currently given like this:
$(
$@
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Fermat's Last Theorem
On 17/04/2023 12:59, Glauco wrote:
|- A. a e. NN A. b e. NN A. c e. NN A. n e. ( ZZ>= ` 3 )
( ( a ^ n ) + ( b ^ n ) ) =/= ( c ^ n )
I think I'd prefer
|- A. a e. NN A. b e. NN A. c e. NN A. n e. NN
( ( ( a ^ n ) + ( b ^ n ) ) = ( c ^ n ) -> n <= 2 )
since it shows where the cutoff
If I'm not mistaken, a possible formalization of
https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem
in set.mm would be
|- -. E. a e. NN E. b e. NN E. c e. NN E. n e. ( ZZ>= ` 3 ) ( ( a ^ n ) + (
b ^ n ) ) = ( c ^ n )
or
|- A. a e. NN A. b e. NN A. c e. NN A. n e. ( ZZ>= ` 3 ) ( ( a ^ n )
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
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 wrote:
> Oooh, thanks. I've been thinking a bit about formalizing n=3 or n=4 in
> metamath (or perhaps more likely,
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
(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
Looks like http://www.ipam.ucla.edu/abstract/?tid=19347=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
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,
