p = 3 case

Stream: FLT

[Pietro Monticone]

Kevin Buzzard said:

1) fermatLastTheoremThree: this is FLT for p=3 and it's being worked on by the LFTCM team e.g. Pietro Monticone . My impression is that it's all under control; the node will go green when the result is in mathlib.

Yes, this is exactly right.

For those interested, here you can find all the relevant resources:

• Zulip Topic.
• Original repository we worked in at LFTCM2024 and from which the porting to Mathlib is happening. Once a PR is merged into Mathlib, the related code is removed from this repository (e.g. #11767).
• Forked repository containing the full project including Github page, documentation and blueprint.

[Ruben Van de Velde]

What's the situation re: landing it in mathlib?

[Riccardo Brasca]

First of all I think we need #12386

[Riccardo Brasca]

It is ready to go in my opinion

[Pietro Monticone]

If I'm not mistaken #11767 is the only PR that has been merged so far.

[Riccardo Brasca]

Yes, then we realized that rings
of integers can be much faster and we focused on that

[Riccardo Brasca]

BTW if someone has time to review #12386 it would be great... :smile:

[Kevin Buzzard]

There seems to be an open question about whether the map from O_K to K should be a coercion?

[Riccardo Brasca]

It now is. Having it as a coercion I don't think can hurt. The problem is that there are two "natural" ways of moving from 𝓞 K to K (using the coercion and algebraMap, of course those are defeq). Making the coercion an abbrev works well and there not that much friction.

[Matthew Ballard]

I think it is fine to cut off the features for that PR and push some things to follow-ons.

[Riccardo Brasca]

@Kevin Buzzard do you want flt3 in the FLT repo or are you happy to wait for it to be merged in mathlib?

[Kevin Buzzard]

I definitely want it in mathlib!

The FLT repo will have some stuff which is too full of sorries to go into mathlib, but my vision is that it's just used as a sandbox for getting things ready for mathlib (e.g. my students' work on families of Galois reps and on Frobenius elements). The smaller the repo, the better!

[Riccardo Brasca]

OK, it will stay in my repo. Don't worry, we will take care of having it in mathlib soon.