Formalizing Fermat's Last Theorem

[Jim Kingdon]

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

[Steven Nguyen]

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.

[Jim Kingdon]

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.

[David Crisp]

(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

[Jim Kingdon]

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).

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/308508e3-2ad5-41ae-b362-1c7aa5983207n%40googlegroups.com.

[Mario Carneiro]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/91add638-5d2d-640c-4314-9c104e205916%40panix.com.

[LM]

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 di....@gmail.com:

[Glauco]

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 ) + ( b ^ n ) ) =/= ( c ^ n )

Glauco

[Paul Chapman]

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 occurs.

Cheers, Paul

[Antony Bartlett]

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

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

$@

  flt @p |- ( ( N e. ( ZZ>= ` 3 ) /\ ( X e. NN /\ Y e. NN /\ Z e. NN ) )

    -> ( ( X ^ N ) + ( Y ^ N ) ) =/= ( Z ^ N ) ) @=

    ? @.

$)

Not that that makes this one particular way of stating it binding or anything.

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f4db70b5-ef66-fdc6-cea6-44c321cbe804%40igblan.free-online.co.uk.