FLT for n=3

Stream: maths

[Kevin Buzzard]

There is a pretty clunky proof arguing only within $\Z$ that the only solutions to $x^3+y^3=z^3$ in integers are the obvious ones, but the natural proof (a descent on the elliptic curve) works in the unique factorization domain $\Z[(1+\sqrt{-3})/2]$. Do we have FLT for $n=3$ in mathlib? A student here who has done a bunch of Lean already is looking for a project and this might be a cool one. But one thing I'm stuck on is that a natural start would be to make this ring (I think it's called the Eisenstein Integers) and prove it's a Euclidean domain (in fact a summer project student did this for me this summer as part of her MSc, but never PR'ed it). But is there a home for this ring in mathlib or are people going to tell me to use the integers of $\mathbb{Q}(\sqrt{-3})$, which will be much harder to work with (but certainly not impossible).

[Alex J. Best]

This was discussed fairly recently in the flt regular stream (no link due to mobile sorry) but it seems @Ruben Van de Velde has it at https://github.com/Ruben-VandeVelde/flt/blob/main/src/euler.lean at least

[Kevin Buzzard]

Oh nice! This looks like the clunky proof :-)

[Eric Rodriguez]

discussion is around here

[Ruben Van de Velde]

Clunky is the right word, certainly. It doesn't quite manage to stay in $\Z$, though Euler may have thought so - I ended up writing more code about $\Z[\sqrt{-3}]$ (which isn't a UFD, but somehow "close enough") than about $\Z$

[Riccardo Brasca]

Also on mobile

[Riccardo Brasca]

But it seems "case I" is doable, but for "case II" one has to work

[Kevin Buzzard]

Actually this issue isn't going away despite FLT3 being done; over the summer I'll have a student thinking about cubic reciprocity and here all the statements are in this ring of Eisenstein integers. Is there a case for just making a new definition? Universe-polymorphic obviously ;-)

[Riccardo Brasca]

In flt-regular we are very close to prove that ring of integers of a cyclotomic extension is what it is. I am sure it will be in mathlib before the summer.