Completion of the FLT regular project

Stream: general

[Floris van Doorn]

Let's start a discussion topic outside the #announce stream.

[Floris van Doorn]

It's great that two projects were finished today!

[Riccardo Brasca]

I've open a thread in the FLT stream, but I guess this thread will also work.

[Pedro Sánchez Terraf]

Congrats again! :tada:

Has the relation between FLT-regular and unrestricted FLT already being discussed in Zulip? I mean, for non-number theorists.
I'm a little curious about the history of the result, if it was actually proved before FLT or the regular version was derived from Wiles' proof.

[Riccardo Brasca]

Unfortunately the full proof of flt is unrelated to the proof in the regular case.
On the other hand, to get to flt-regular we had to develop a lot of algebraic number theory, that is needed anyway to prove Fermat (even if the proof is completely different).

[Andrew Yang]

This is an 1847 result by Kummer, which is way before Wiles. In fact, this result by Kummer (actually the theory behind it) is one of the inspirations that culminated into the modern algebraic number theory we all know and love now.

[Eric Rodriguez]

Pedro Sánchez Terraf said:

Congrats again! :tada:

Has the relation between FLT-regular and unrestricted FLT already being discussed in Zulip? I mean, for non-number theorists.
I'm a little curious about the history of the result, if it was actually proved before FLT or the regular version was derived from Wiles' proof.

There's a fun story that Lamé came into the Paris Academy, proclaiming a wonderful proof of FLT, or well, proclaiming that the factorization a^n + b ^ n = (a + b)(a + ζb)(a + ζ^2 b)... led to a contradiction immediately by the same logic as in the n=3 case proven pretty famously by Euler (whose proof was reproduced by @Ruben Van de Velde, and we used!). Then Liouville stood up and basically said "no it doesn't, we may not even have unique factorization", leading Kummer to then say that he has already done all the work to prove what we essentially proved in this project, and get the most possible out of this idea of factorizing. Regularity is a sufficient condition for the rescuing of Lamé's "proof", well at least in the case where ¬p|abc; the more technically intensive p|abc requires new ideas, and is what was just finished being proved.

[Eric Rodriguez]

Most of the history of this stuff is in Harold M. Edwards' Fermat's Last Theorem, a genetic introduction to Algebraic Number Theory and maybe another paper he did whose name slips my mind; they're really interesting reads.

[Eric Rodriguez]

For one example of what Andrew points out, ideals (not in their modern form, I think as normal numbers of the Hilbert Class Field?) were developed by Kummer for this

[Riccardo Brasca]

I think that originally Kummer's included what is nowadays called kummer's lemma in the definition of a regular prime and only later it was realized that this is automatic. Assuming Kummer's lemma, case II is similar to case I (even if it is more involved, the main ideas are the same).

Kummer's lemma is what makes case II really harder.

[Kevin Buzzard]

Congratulations all!

I need the n=3 case for FLT-Wiles because Mazur doesn't rule out the Frey curve having 3-torsion. Are there plans to get the n=3 case into mathlib?

[Ruben Van de Velde]

I was planning to ask you whether you needed it, and if so, pick that up again :)

[Riccardo Brasca]

All the project will end up in mathlib, that's a promise!

n=3 is self contained and it's here

[Kevin Buzzard]

Yeah I know where it is, I just can't use it right now :-)

[Pedro Sánchez Terraf]

Eric Rodriguez said:

There's a fun story that Lamé came into the Paris Academy, proclaiming a wonderful proof of FLT, or well, proclaiming that the factorization a^n + b ^ n = (a + b)(a + ζb)(a + ζ^2 b)... led to a contradiction immediately by the same logic as in the n=3 case proven pretty famously by Euler (whose proof was reproduced by Ruben Van de Velde, and we used!). Then Liouville stood up and basically said "no it doesn't, we may not even have unique factorization",

Oh, this is the “lacune à remplir” business... Thanks!

[Ruben Van de Velde]

The other option is to build the theory to prove that 3 is a regular prime, but I don't know if that's the best use of time (or who'd do it, for that matter)

[Riccardo Brasca]

We are very close to Minkowski bound, and once we have it it should be easy to prove that $\mathbb{Q}(\zeta_3)$ is a PID, then we can follow the modern proof (that is still done by hand)

[Riccardo Brasca]

Ruben Van de Velde said:

The other option is to build the theory to prove that 3 is a regular prime, but I don't know if that's the best use of time (or who'd do it, for that matter)

This does not work unfortunately. There is a subtle point were we need p > 3 in the proof, and that's unavoidable I think.

[Kevin Buzzard]

Heh, same is true for Wiles' proof.

[Riccardo Brasca]

But knowing that $\mathbb{Q}(\zeta_3)$ is a PID still hepls. Something like this
I think is more or less @Ruben Van de Velde 's proof, but it's more readable.

[Kevin Buzzard]

Yeah the proof in Hardy and Wright exploits unique factorisation in Z[zeta_3]. It's then just a descent on an elliptic curve.

[Riccardo Brasca]

p>3 is needed in case 1, so (given a proof that 3 is regular) we automatically have that there are no solutions such that 3 divides a*b*c

[Yaël Dillies]

And then you're done mod 9, right?

[Anne Baanen]

Congratulations everyone! I look forward to helping to move all your hard work into Mathlib :)

[Riccardo Brasca]

Yaël Dillies said:

And then you're done mod 9, right?

Yes, this is probably the shortest path using our proof.

[Filippo A. E. Nuccio]

Congrats, this is really a great arithmetic achievement! :numbers:

[Antoine Chambert-Loir]

Kevin Buzzard said:

Heh, same is true for Wiles' proof.

I think wiles's proof also needs n = 4. (Which was known to Fermat, and for which he gave us a proof.)

[Yaël Dillies]

This is actually already in mathlib: docs#fermatLastTheoremFour