Special cases of Fermat's Last Theorem

Stream: Is there code for X?

[Roman Bars]

I suppose it will be a miracle if Wiles-Taylor's proof is formalized within the next 5 years. But what about Kummer's argument for regular primes or the more elementary arguments for specific exponents? Are any of those formalized?

[Johan Commelin]

I think @Paul van Wamelen worked on n = 4?

[Johan Commelin]

And others tried n = 3

[Ruben Van de Velde]

I did most of Euler's elementary proof of n = 3, but got stuck on the step https://fermatslasttheorem.blogspot.com/2005/05/fermats-last-theorem-n-3-key-lemma.html

[Ruben Van de Velde]

n=4 is docs#not_fermat_4

[Ruben Van de Velde]

(I assume @Kevin Buzzard has thoughts on Wiles)

[Kevin Buzzard]

It will be impressive if we can even state the main steps of the Wiles-Taylor proof within the next five years, let alone prove anything. I would need a post-doc working full time on it

[Kevin Buzzard]

It would take a couple of years to do, I guess. I've been thinking about modular curves etc. The first goal would be statements of things like semistable taniyama-shimura and R=T theorems where no data is sorried

[Kevin Buzzard]

Even defining modular curves X_0(N) is hard because of cusps and representability issues

[Alex J. Best]

Roman Bars said:

But what about Kummer's argument for regular primes or the more elementary arguments for specific exponents? Are any of those formalized?

Class groups are a recent innovation in mathlib (https://arxiv.org/pdf/2102.02600.pdf) so this argument is only really possible as of quite recently (its been possible to define regular primes for a while via Bernoulli numbers I suppose, but really you need the class group for this argument).