Port to Lean4

Stream: FLT-regular

[Riccardo Brasca]

In half an hour #5447 will land in mathlib4. I think this is the last missing piece to be able to port the whole project to Lean4.

I am going to Copenhagen tomorrow, so I think I will start the port next Monday. We will see how difficult it is :)

[Riccardo Brasca]

I am starting the port. I think the easiest way is to create a github repo with the output of mathport and then fix everything. I will make it public as soon as it exists (hopefully today). Let me know if you want invitations to contribute :)

[Riccardo Brasca]

https://github.com/riccardobrasca/flt-regular

It was surprisingly easy

[Riccardo Brasca]

Mathlib seems to work!

[Ruben Van de Velde]

Nice! I'd ported the n=3 bits already, so you could c/p those parts

[Riccardo Brasca]

That's good! Is it ok for you if we just copy/paste your repo to flt-regular?

[Ruben Van de Velde]

Sure! https://github.com/Ruben-VandeVelde/flt4

[Riccardo Brasca]

Thanks!

[Chris Birkbeck]

I cloned the repo to see how this works. infoview is currenty saying "info: [538/1712] Building Mathlib.Algebra.Order.Sub.WithTop" etc, is this normal?

[Eric Rodriguez]

did you do the lake exe cache stuff? im not sure how it works on projects ngl

[Riccardo Brasca]

Yes, it's a normal lean4 repo (I hope). So you need to get the cache.

[Chris Birkbeck]

ok let me try that

[Kevin Buzzard]

Eric Rodriguez said:

did you do the lake exe cache stuff? im not sure how it works on projects ngl

It works fine on projects ( and it's lake exe cache get)

[Chris Birkbeck]

Ok so I ran lake exe cache get and restarted the server. It seemed to fix that. I now have lots of red in the infoview, but maybe this is because the port is in progress?

` c:\Users\chris\.elan\toolchains\leanprover--lean4---nightly-2023-06-20\bin\lake.exe print-paths Init FltRegular.MayAssume.Lemmas FltRegular.NumberTheory.Cyclotomic.Factoring FltRegular.NumberTheory.Cyclotomic.UnitLemmas FltRegular.NumberTheory.Cyclotomic.CaseI` failed:

stderr:
info: [1296/1712] Building FltRegular.FltThree.Primes
info: [1297/1712] Building FltRegular.FltThree.OddPrimeOrFour
info: [1350/1712] Building FltRegular.ReadyForMathlib.Homogenization
info: [1652/1712] Building FltRegular.Norm.NormPrime
info: [1658/1712] Building FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
error: > LEAN_PATH=.\build\lib;.\lake-packages\proofwidgets\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\chris\.elan\toolchains\leanprover--lean4---nightly-2023-06-20\bin\lean.exe .\.\.\FltRegular\FltThree\Primes.lean -R .\.\. -o .\build\lib\FltRegular\FltThree\Primes.olean -i .\build\lib\FltRegular\FltThree\Primes.ilean -c .\build\ir\FltRegular\FltThree\Primes.c
error: stdout:
.\.\.\FltRegular\FltThree\Primes.lean:17:7: error: failed to infer 'let' declaration type
.\.\.\FltRegular\FltThree\Primes.lean:17:39: error: don't know how to synthesize implicit argument
@IsCoprime.pow R CommRing.toCommSemiring x y ?m.1527 ?m.1528 hxx
context:
``
or maybe something else is wrong

[Chris Birkbeck]

Ok yes I think its because its trying to import files that have errors from porting

[Riccardo Brasca]

Yes, I didn't fix anything yet

[Riccardo Brasca]

So it's not working at all, it's the standard output of mathport

[Chris Birkbeck]

Ok cool, thats what I thought. At least the FltThree bits should be working, but I guess you havent copy pasted it in yet?

[Riccardo Brasca]

Yes, I didn't do it. I just invited you to the repo, so feel free to push whatever fix you did.

[Riccardo Brasca]

I will report here the files I am working on, to avoid duplicating effort:

• FltRegular.Norm.NormPrime: done.
• ReadyForMathlib.Homogenization: done.
• NumberTheory.Cyclotomic.Factoring: done.
• NumberTheory.Cyclotomic.CyclotomicUnits: done.
• NumberTheory.Cyclotomic.GaloisActionOnCyclo: done.
• NumberTheory.Cyclotomic.ZetaSubOnePrime: done.
• NumberTheory.Cyclotomic.UnitLemmas: done.
• NumberTheory.Cyclotomic.CyclRat: done.
• NumberTheory.RegularPrimes: done.
• NumberTheory.KummersLemma: done.
• MayAssume.Lemmas: done.
• CaseII.Statement: done.
• NumberTheory.Cyclotomic.CaseI: done.
• CaseI.AuxLemmas: done.
• CaseI.Statement: done.
• FltRegular: done.

[Riccardo Brasca]

The project is fully ported!

[Riccardo Brasca]

It is sometimes very slow, but we can live with it at the moment.

[Johan Commelin]

Wow, that was fast!!

[Eric Rodriguez]

bumping to current Std/Mathlib seems to build fine

[Eric Rodriguez]

should we move this to leanprover-community soon?

[Riccardo Brasca]

Yes, I think we can just use the old flt-reguler repo, I don't see any point in keeping the Lean3 version

[Riccardo Brasca]

(we can clone it somewhere just for the record)

[Ruben Van de Velde]

We could rename the existing master branch to lean3

[Ruben Van de Velde]

Meanwhile Kevin submitted a PR for the general case to mathlib4(*)

(*) statement only

[Eric Rodriguez]

What PR?

[Chris Birkbeck]

#6508 I think

[Riccardo Brasca]

I am not sure I did all the git magic right, but we should now have:

• the master branch, with the latest mathlib3 (and all the blueprint, graph)
• a mathlib3 branch, equal to master
• a mathlib4 branch, that is a valid Lean4 repo, with a ported project (with a very recent mathlib4, it is even slower that one month ago)

[Ruben Van de Velde]

:champagne:

[Ruben Van de Velde]

Is the ReadyForMathlib ready for mathlib? I might look at creating a PR

[Riccardo Brasca]

At the moment, it only contains stuff about homogeneous polynomial written by @Alex J. Best

[Eric Rodriguez]

It'd be really nice to have it in mathlib, maybe in the generality of weighted homogeneous polys