Fermat Last Theorem for regular primes

Stream: maths

[Riccardo Brasca]

Dear all,
together with @Alex J. Best, @Chris Birkbeck and @Antoine Chambert-Loir we are interested proving the Fermat Last Theorem for regular primes. Of course everyone is very welcome to join the project, it would be nice to run it similarly to a (very) small LTE. I think Alex already has some code, but we didn't do anything serious until now, so if you are already working on this please let us know.

[Johan Commelin]

Great idea!

[Johan Commelin]

Do you already have a repo?

[Riccardo Brasca]

I am trying to understand what is the best option to do it

[Riccardo Brasca]

All suggestions are very welcome

[Johan Commelin]

leanproject new flt-regular

[Johan Commelin]

And then you need to create an empty repo on github and push it there.

[Johan Commelin]

If you want to host it on the leanprover-community organization, I can create a repo for you.

[Riccardo Brasca]

That would be awesome!

[Johan Commelin]

Do you like flt-regular as name? Or do you want something else? regular-fermat?

[Chris Birkbeck]

That would be great. I'm trying to sort out a rough tex file to make a blueprint out of.

[Johan Commelin]

If you give me a name, I'll give you a repo (-;

[Riccardo Brasca]

flt-regular is perfect

[Chris Birkbeck]

I like flt-regular.

[Johan Commelin]

https://github.com/leanprover-community/flt-regular

[Johan Commelin]

https://github.com/leanprover-community/flt-regular/invitations

[Johan Commelin]

So now, after you do leanproject new flt-regular and cd into the new directory, you should do

git remote add origin git@github.com:leanprover-community/flt-regular.git
git add whatever_leanproject.created
git commit -am 'initial commit'
git push -u origin master

[Johan Commelin]

You can also consider creating a new stream. But you can of course also use #maths for the time being.

[Johan Commelin]

First question: which definition of regular prime do you plan to use?

[Riccardo Brasca]

My idea was to use the class number. We need #9071, but that's going to be in mathlib quite soon I guess. The real first problem is the ring of integers of cyclotmic fields

[Riccardo Brasca]

We still have to discuss a good strategy :smile:

[Yaël Dillies]

I love how I can just throw ideas around and someone makes a project out of it :grinning:

[Johan Commelin]

It's probably the better definition to work with. But will we be able to show that is irregular?

[Johan Commelin]

Yaël Dillies said:

I love how I can just throw ideas around and someone makes a project out of it :grinning:

It was Riccardo's idea, right? https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Cyclotomic.20fields/near/258814613

[Yaël Dillies]

Riccardo Brasca said:

So maybe it's time for regular primes? This seems an ambitious but not out of reach project.

It was, but I seem to have provoked it :wink:

[Riccardo Brasca]

I am really sad that 37 is irregular

[Johan Commelin]

#9071 depends on #9606 which seems to be blocked pretty badly.

[Johan Commelin]

There are some very nasty timeouts going on there.

[Johan Commelin]

Riccardo Brasca said:

I am really sad that 37 is irregular

Why? I think irregularity is indirectly a raison d'être for the emoji.

[Eric Rodriguez]

BTW, we can define regularity for all numbers, right?

[Riccardo Brasca]

Johan Commelin said:

Riccardo Brasca said:

I am really sad that 37 is irregular

Why? I think irregularity is indirectly a raison d'être for the emoji.

Just because it means we are not proving FLT for 37!

[Johan Commelin]

OH NOOO!! There is a for_mathlib/ directory already :rofl:

[Johan Commelin]

@Patrick Massot Can you please make creation of this directory part of leanproject new? [/joking]

[Riccardo Brasca]

Ahahah it's the first directory I created! :grinning_face_with_smiling_eyes:

[Ruben Van de Velde]

Johan Commelin said:

#9071 depends on #9606 which seems to be blocked pretty badly.

We should probably reverse the dependency, since #9606 indeed is not doing well

[Johan Commelin]

Is that possible? I thought that #9071 couldn't do without it...

[Adam Topaz]

Sounds like a fun project! If I recall correctly cyclotomic 0 is 1, and adjoin_root f is defined to be K[X]/(f), so

instance (n : ℕ) : field (cyclotomic_field n) := sorry

is false for n = 0.

[Kevin Buzzard]

This just seems like something which is about positive integers and there is no coherent way to include n=0.

[Adam Topaz]

Sure, I was just commenting about one of the sorry's from the brand new for_mathlib folder :)

[Adam Topaz]

Maybe cyclotomic_field 0 should be defined to be $\mathbb{Q}$?

[Adam Topaz]

Or $\overline{\mathbb{Q}}$ since every algebraic number is a $0$-th root of unity? :thinking:

[Eric Rodriguez]

For the cyclotomic stuff, please look at my recent PRs because they were made for the purpose of cyclotomic fields anyways

[Eric Rodriguez]

I think the best option is, as Johan mentioned on one of them, to have an API for the generator of cyclic groups

[Adam Topaz]

Are these the PRs that Johan mentioned above?

[Johan Commelin]

Nope, that's the PR about class numbers

[Adam Topaz]

Oof, why does #9606 break something about cech_nerves?

[Kevin Buzzard]

I don't think there's a non-crazy definition of $\phi(0)$ ("naturals less than n coprime to n" gives 0, "order of units in $\Z/n\Z$" gives 2) and I don't think there's a non-crazy definition of $\Phi_0$ either, you are somehow dividing by 0 to get there.

[Adam Topaz]

Sure, but I do think there's a non-crazy definition of $\mathbb{Q}(\mu_0)$. Namely: $\overline{\mathbb{Q}}$

[Adam Topaz]

Anyway, this is silly. No one should ever use $\mu_0$.

[Kevin Buzzard]

Surely the max abelian extension, not the max algebraic extension?

[Kevin Buzzard]

Surely $\mu_0$ is affine 1-space ;-) It represents $\{r\in R\,|\,r^0=1\}$.

[Adam Topaz]

Exactly, that's why $\mathbb{Q}(\mu_0(\overline{\mathbb{Q}})) = \overline{\mathbb{Q}}$.

[Johan Commelin]

Unfortunately roots_of_unity 0 is empty in mathlib...

[Adam Topaz]

Oh no! All the junk values are inconsistent.

[Reid Barton]

I was about to say, I bet you could fix that easily by setting $\mu_0 = \mu_{37}$ etc.

[Kevin Buzzard]

So there are two questions here -- the funny one, which we've all been indulging in, giving random semi-plausible definitions for all these things at the junk input 0, but there's also the serious one, which is what we should actually do with the definitions. I feel like the definitions are all going to be of the form "if n = 0 then return the following junk value else return the sensible value"

[Kevin Buzzard]

actually that's a really good idea. Why not just let the value for 0 be the value for 1 in all cases?

[Kevin Buzzard]

Then all the theorems are guaranteed to remain true

[Johan Commelin]

I guess that shifts the question to what you mean by "all cases".

[Reid Barton]

Also pnat is a thing but I guess that's heresy to suggest

[Johan Commelin]

Does this include $φ(0)$?

[Johan Commelin]

Because that's defined outside of "number theory". No idea what mathlib does there right now.

[Kevin Buzzard]

I guess it would do. My guess is that setting 0=1 is easier than working with pnat but I might be wrong.

[Reid Barton]

Kevin Buzzard said:

setting 0=1 is easier

Yes this makes a lot of things easier actually

[Adam Topaz]

I wish there was more love for pnat.

[Kevin Buzzard]

Maybe this is a good time to try it?

[Kevin Buzzard]

The reason for defining junk values usually is to spare us from having to say "oh and also assume $n\not=0$" in 100 places, but if n : pnat then we don't have to say this

[Adam Topaz]

E.g. we should probably write down a multiplicative recursor for pnat based on docs#multiset.induction or something.

[Riccardo Brasca]

I tried to use pnat when defining cyclotomic polynomials, but it ended up being quite annoying since the API is not as complete as for nat.

[Kevin Buzzard]

Right, but if it's just missing lemmas then they can be added. However if it's that we want to use ring then this is more problematic

[Johan Commelin]

maybe ring should work for arbitrary commutative distribs?

[Kevin Buzzard]

This is the sort of thing which it's easy for me to say, but then someone like Rob or Mario maybe pops up and says "actually that would be a ton of work for very little benefit"

[Eric Rodriguez]

One of the primitive roots things is in pnat, so it's definitely at least worth considering. Some PRs of interest: #9778, #9779

[Eric Rodriguez]

(these are the ones I meant earlier)

[Johan Commelin]

How maths-hard is the proof that cyclotomic regular is equivalent to Bernoulli regular?

[Riccardo Brasca]

BTW we have a sorry free def of regular prime (or regular number if you prefer). The class number of an extension of Z is essentially already in mathlib.

[Thomas Browning]

I would be very interested in joining this project. Is there anything I should do, or should I just start working on flt-regular?

[Johan Commelin]

But provig that 37 is irregular is probably easier with the Bernoulli defn

[Kevin Buzzard]

IIRC cyclo regular = Bernoulli regular is proved using the analytic class number formula, so we're blocked by complex analysis

[Johan Commelin]

I guess reading Chris's blueprint is a good start?

[Thomas Browning]

Washington's Introduction to cyclotomic fields is THE reference for this sort of stuff

[Riccardo Brasca]

@Johan Commelin can you add a flt_regular stream? So we can speak without spamming everyone

[Johan Commelin]

I think anyone can

[Kevin Buzzard]

The more refined statement, that $p$ divides $B_k$ iff $p$ divides the $k$ th part of the class group was not known until Ribet's work which used congruences of modular forms.

[Thomas Browning]

Kevin Buzzard said:

The more refined statement, that $p$ divides $B_k$ iff $p$ divides the $k$ th part of the class group was not known until Ribet's work which used congruences of modular forms.

Herbrand's direction isn't as hard though, right?

[Kevin Buzzard]

and modular forms are also blocked by complex analysis ;-)

[Johan Commelin]

@Riccardo Brasca let me know if Zulip does not permit you to create a stream

[Chris Birkbeck]

Johan Commelin said:

I guess reading Chris's blueprint is a good start?

Im still trying to get this working, so there isnt much to read at the moment :P

[Kevin Buzzard]

I've created streams, even private streams, so I guess anyone can do it

[Riccardo Brasca]

I think someone gave you the permission for the Xena stream, I don't see the "create stream" button mentioned here

[Thomas Browning]

I made a stream a while ago, but can't seem to figure out how to do it anymore. Maybe permissions have changed.

[Chris Birkbeck]

Kevin Buzzard said:

and modular forms are also blocked by complex analysis ;-)

Well, technically "only" non-zero modular forms are blocked! :stuck_out_tongue:

[Johan Commelin]

@Riccardo Brasca @Chris Birkbeck @Alex J. Best #FLT regular

[Riccardo Brasca]

Thank you!

[Johan Commelin]

(Sorry, I was away for dinner. Otherwise I would have created it an 45 min ago.)

[Riccardo Brasca]

We've just finished the proof of the so called caseI of Fermat's last theorem for regular prime.

theorem caseI {a b c : ℤ} {p : ℕ} (hpri : p.prime) (hreg : is_regular_number p hpri.pos)
  (hodd : p ≠ 2) (caseI : ¬ ↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p :=
...

#print axioms caseI --propext quot.sound classical.choice

Thanks to everybody involved!

CaseII will be significantly harder though...

[Patrick Massot]

We really need #print actual_axioms so that the output is easier to read.

[Patrick Massot]

I also have trouble reading caseI without thinking case and then unfreeze the instance cache, but I guess this is a more specialized perversion.

[Riccardo Brasca]

Well, we will PR all of this to mathlib at some point, and we will think about better names...

[Kevin Buzzard]

Yeah that's what we said about the perfectoid project

[Yaël Dillies]

How many lines is the project now?

[Riccardo Brasca]

I am not sure how it counts, but this site says 6746. But note that a lot of stuff (notably the ring of integers of cyclotomic fields, that have been defined thanks to the project) is already in mathlib.

[Yaël Dillies]

Oh that's not so much! The perfectoid project was about 15k, right? I still have faith that you could get it all in mathlib then.

[Riccardo Brasca]

Yes, we tried to PR as much as possible from the beginning. I think that fr projects of this size is the best strategy, if one is not too in a hurry.

[Kevin Buzzard]

Not all the perfectoid project should be in mathlib, but the for_mathlib directory should be. To Patrick's credit, all the stuff he put in it is now in mathlib. I didn't get around to doing my part yet though :-(

[Ruben Van de Velde]

Kevin Buzzard said:

Not all the perfectoid project should be in mathlib

Perhaps a silly question from someone who doesn't know what a perfectoid is: why not?

[Kevin Buzzard]

Well I guess I mean "perfectoid spaces are a bit niche and I am not sure that I could coherently argue that they should be in a maths library", but I guess that since 2019 we got plenty of other niche things. Maybe one day they'll be there, but a lot of that code is not really for human consumption.

[Scott Morrison]

Write once, read never.

[Kevin Buzzard]

It was just a publicity stunt, it wasn't supposed to be read :-)