Zulip Chat Archive

Stream: Is there code for X?

Topic: Special cases of Fermat's Last Theorem


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

view this post on Zulip Johan Commelin (Feb 10 2021 at 08:30):

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

view this post on Zulip Johan Commelin (Feb 10 2021 at 08:30):

And others tried n = 3

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

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 08:36):

n=4 is docs#not_fermat_4

view this post on Zulip Ruben Van de Velde (Feb 10 2021 at 08:39):

(I assume @Kevin Buzzard has thoughts on Wiles)

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

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

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 08:44):

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

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