Zulip Chat Archive

Stream: maths

Topic: Fermat's Last Theorem for n=4


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 17 2020 at 12:15):

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

view this post on Zulip Paul van Wamelen (Sep 17 2020 at 12:17):

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

view this post on Zulip Johan Commelin (Sep 17 2020 at 12:19):

@Riccardo Brasca Oops, too bad

view this post on Zulip Johan Commelin (Sep 17 2020 at 12:20):

However, there are plenty other interesting topics.

view this post on Zulip Ruben Van de Velde (Sep 17 2020 at 12:21):

I'm poking at n=3, fwiw

view this post on Zulip 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.

view this post on Zulip Riccardo Brasca (Sep 17 2020 at 12:24):

ops, I didn't see you answer :)

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 17 2020 at 12:44):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:19):

no

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:21):

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

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:21):

or in any ring

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:22):

Z

view this post on Zulip Johan Commelin (Sep 17 2020 at 13:25):

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

view this post on Zulip Johan Commelin (Sep 17 2020 at 13:25):

map_witt_polynomial is a simp-lemma that absorbs mv_polynomial.map

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:29):

there are only 6 units in Z[ω]

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:29):

and in each case you should get a contradiction

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:29):

Kenny the proof is a descent, it's delicate

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 17 2020 at 13:30):

there are delicate local-global principles involved

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:30):

what's wrong with my proof?

view this post on Zulip Kenny Lau (Sep 17 2020 at 13:31):

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

view this post on Zulip Thomas Browning (Sep 17 2020 at 19:20):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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: May 14 2021 at 20:13 UTC