Stream: Is there code for X?

Topic: Special cases of Fermat's Last Theorem

Roman Bars (Feb 10 2021 at 08:26):

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 (Feb 10 2021 at 08:30):

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

Johan Commelin (Feb 10 2021 at 08:30):

And others tried n = 3

Ruben Van de Velde (Feb 10 2021 at 08:35):

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 (Feb 10 2021 at 08:36):

n=4 is docs#not_fermat_4

Ruben Van de Velde (Feb 10 2021 at 08:39):

(I assume @Kevin Buzzard has thoughts on Wiles)

Kevin Buzzard (Feb 10 2021 at 08:41):

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 (Feb 10 2021 at 08:43):

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 (Feb 10 2021 at 08:44):

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

Alex J. Best (Feb 10 2021 at 11:28):

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).

Last updated: May 17 2021 at 16:26 UTC