Mathlib on Lean4

Stream: new members

[Brandon Bocanegra]

Will mathlib become compatible with Lean 4 any time soon? Or do we have to stick with the community version of Lean 3?

[Johan Commelin]

There are all sorts of preparations (refactors/backports) being made to prepare for porting mathlib to Lean 4. The hope/plan is to have a porting fest in the summer.

[Johan Commelin]

@Brandon Bocanegra So for the next few months, it will definitely still be Lean 3, but afterwards hopefully Lean 4

[Scott Morrison]

(my guess is that this is very ambitious, and you might be looking at the summer after that... I'd love to be wrong)

[Mario Carneiro]

Yeah, I think it is more likely that by the end of the summer we have a good idea how to actually port files and have some minimal core of mathlib working

[Kevin Buzzard]

My impression is that we're all going round saying "woo Lean 4 is released" but I think that this statement needs to be put into some important context. What has happened is that we have a milestone release to play with but it's also manifestly clear that Leo and others are still working really hard and making a bunch of changes -- they released it because they want user feedback, they want people to do little experiments to find out what is working well and what is not working so well (they have made all sorts of changes since Lean 3, it might be the same type theory but stuff like heterogeneous addition and changes to the typeclass system and unhygienic terms and many other things are all major changes). Until Leo is actually happy with Lean 4 (and given that there are several commits every day it's absolutely clear that he does not think that this project is finished and so he is not happy!) there is in some sense no point in even beginning to port mathlib -- I mean it's great to experiment, but if 80% of it gets ported by some magic code and then Leo decides to change something fundamental then maybe it all breaks and we're back to square one. My impression from a brief discussion with Leo about this is that he absolutely does not want to rule out the possibility that by summer he is still changing the fundamentals of the system, and I am absolutely certain that he will not want to be hampered by the mathlib crowd going "but if you do this then everything will break", which is what happened when we went from 3.4.0 to 3.4.1 with the issue about type classes after the colon. I would suggest that one way of thinking about this porting question is that until the Lean devs actually come out with some sort of release where they are prepared to say "we are now happy with the basics, and we have seen sufficiently many small projects written in Lean 4 to be convinced that the system is as powerful and flexible as we believe it should be, and we will not be making several commits every day some of which change absolutely fundamental parts of the system" then we should not really be jumping the gun and asking questions about when porting mathlib is actually going to happen. Sure we can think about it but right now I think it's very important to be patient.

I have been playing with Lean 4. I really like it. It is at the stage where as a prover there are no problems in doing little projects like getting sets and filters and equiv working -- indeed I have been playing with sets and filters here and with equiv here, typically live streaming on the discord with people like Jason KY and Shing Tak Lam and Yakov Perchersky watching and giving me advice and insight. Leo already told me personally that the filter project revealed a little issue with Lean 4 which he fixed, and as a mathematician who knows nothing about programming I am a little bit proud that I could contribute in this way. Based on this I would suggest that a really interesting and fun way to make progress would be to start a completely unofficial experimental repo where people just port mathlib files, or even just parts of mathlib files, from Lean 3 over to Lean 4. I have a repo where I didn't even start -- maybe I should make it public. I will be doing some porting of basic files myself, but it's not a priority project for me right now, it's just something I'm playing with in my spare time and I have several serious Lean 3 things to think about right now (liquid stuff, stacks stuff, ext and tor and group cohomology...). But my impression is that this is the correct question right now -- we are still very much in the experimental phase and it is only after we all understand what Lean 4 should be (Lean 4 exists, but still might change fundamentally) that we can start to think about the glorious port.

OK I made an empty repo public: PRs are welcome at https://github.com/kbuzzard/mathlib4_experiments . I will move my work on sets and filters and equivs over at some point.

[Julian Berman]

Are the discord streams public?

[Kevin Buzzard]

no it's a private discord server but you're welcome to have an invite if you want. It's mostly undergraduates and mostly mathematicians but we have some CS people and some people with proper jobs and everything

[Julian Berman]

I'd love one!