Zulip Chat Archive

Stream: maths

Topic: Fermat's Last Theorem for n=4

Riccardo Brasca (Sep 17 2020 at 12:14):

Do we already have a proof of Fermat's last theorem for exponent 4 in Lean? I wasn't able to find it in mathlib and I would try to do it by myself. Since we already have the classification of pythagorean triples, this seems doable.

Johan Commelin (Sep 17 2020 at 12:15):

Nope, I haven't heard of any proof. I think it's open (-;

Paul van Wamelen (Sep 17 2020 at 12:17):

I'm in the process of PR'ing it.

Johan Commelin (Sep 17 2020 at 12:19):

@Riccardo Brasca Oops, too bad

Johan Commelin (Sep 17 2020 at 12:20):

However, there are plenty other interesting topics.

Ruben Van de Velde (Sep 17 2020 at 12:21):

I'm poking at n=3, fwiw

Riccardo Brasca (Sep 17 2020 at 12:24):

@Paul van Wamelen are you working also on the exponent 3? This is of course harder, but I can start trying to do something about Eisensten integers following what we already have for the gaussian integers.

Riccardo Brasca (Sep 17 2020 at 12:24):

ops, I didn't see you answer :)

Johan Commelin (Sep 17 2020 at 12:35):

@Riccardo Brasca Here are some topic ideas:
Polynomials:
What do you think of defining the cyclotomic polynomials, and showing that they are irreducible? Or the binomial polynomials? Or the Fibonacci polynomials?
Some people were thinking about working on the solution of degree 3 or 4 polynomials. Don't know how far they got.

Number theoretic
If you would rather stick to something number theoretic: I don't think we have the Moebius function.
On the more advanced side, people are working on Dedekind domains.
On the local side, we have DVRs, but not yet complete DVRs.
I would love to see a bunch of equivalent definitions of Henselian rings.

Groups
@Chris Hughes I think you proved that A_5 is a simple group. Did this end up in mathlib?
I don't think we have solvable groups.
I don't think we have a classification of finite groups of cardinality < n, for any n greater than 1.

Riccardo Brasca (Sep 17 2020 at 12:38):

@Johan Commelin I was looking for cyclotomic polynomials right now. I will try to prove the irreducibility. I am a little scared about giving the definition, but I will ask here if I get in troubles. (I mean, not the mathematical definition, but how to write it in Lean...)

Johan Commelin (Sep 17 2020 at 12:44):

We also don't know that (multivariate) polynomials are determined by their values on all inputs, if the coefficient ring is infinite.

Johan Commelin (Sep 17 2020 at 12:44):

But this is probably not a nice proof if you are just getting started

Kevin Buzzard (Sep 17 2020 at 13:16):

@Kenny Lau @Patrick Lutz did either of you do any cyclotomic stuff in your Galois theory work?

Kenny Lau (Sep 17 2020 at 13:19):

Kevin Buzzard (Sep 17 2020 at 13:21):

Do you think cyclotomic n should have coefficients in Z or Q?

Kevin Buzzard (Sep 17 2020 at 13:21):

or in any ring

Kenny Lau (Sep 17 2020 at 13:22):

Johan Commelin (Sep 17 2020 at 13:25):

We defined witt_polynomial to have coefficients in any ring. It worked quite well.

Johan Commelin (Sep 17 2020 at 13:25):

map_witt_polynomial is a simp-lemma that absorbs mv_polynomial.map

Paul van Wamelen (Sep 17 2020 at 13:27):

I did start working on n=3. I have that the eisenstein integers is an euclidean domain. But then I realized that fermat n=3 doesn't use the eisenstein integers. At least the usual argument in the cyclotomic ring when it is a UFD doesn't seem to work for n=3. If someone knows a proof of fermat for n=3 using the eisenstein integers, I'd love to see it!

Kenny Lau (Sep 17 2020 at 13:28):

x^3+y^3=z^3 means N(x+ωy) = N(z) so z = u(x+ωy) where u is a unit

Kenny Lau (Sep 17 2020 at 13:29):

there are only 6 units in Z[ω]

Kenny Lau (Sep 17 2020 at 13:29):

and in each case you should get a contradiction

Kevin Buzzard (Sep 17 2020 at 13:29):

Kenny the proof is a descent, it's delicate

Kevin Buzzard (Sep 17 2020 at 13:30):

it's a phi-descent on an elliptic curve, where phi is an isogeny of degree 3.

Kevin Buzzard (Sep 17 2020 at 13:30):

there are delicate local-global principles involved

Kenny Lau (Sep 17 2020 at 13:30):

what's wrong with my proof?

Kenny Lau (Sep 17 2020 at 13:31):

aha, x^3+y^3 isn't the norm of x+ωy lol

Thomas Browning (Sep 17 2020 at 19:20):

We haven't done any cyclotomic fields in our Galois theory stuff

Riccardo Brasca (Sep 17 2020 at 19:29):

@Thomas Browning I will work on cyclotomic polynomial in the next days, without doing anything really sophisticated, but I will be interested in doing some Galois stuff if you need help.

Joseph Myers (Sep 17 2020 at 19:34):

@Paul van Wamelen There's a proof of Fermat for n=3 using Eisenstein integers in Hardy and Wright (section 13.4).

Paul van Wamelen (Sep 17 2020 at 20:01):

Thanks!
It would be quite the adventure formalizing that proof...
@Ruben Van de Velde what proof are you formalizing?

Last updated: Dec 20 2023 at 11:08 UTC