Different lean versions in mathlib

Stream: new members

[Will Fourie]

Morning everyone (for which it is morning). I am quite new to Lean, only started playing around with it the past month or so (worked my way through the tutorial, some small theorems like Cauchy in R iff convergent, and am now working my way through Mathematics in Lean).

I have a vague eventual goal of being able to add something to the maths library, but my maths is quite rusty so for the moment I plan to simply use this to work through some old textbooks (so I can check I am e.g. getting the exercises correct). This is just something fun for me to do on the side, but I am aware that formalising things can take quite a while so my "for the moment" goal may stick around for probably months at least.

My question therefore is to do with how the different lean versions affect my ability to continue with a long-term project like this. Will mathlib switch over to lean 4 at some point, then to lean 5, 6, etc? If so, how drastic are the changes likely to be between the versions - should it still be backwards compatible enough that I can lift code from one version and run it in another?

More to the point, can the maths library lift things from one version to run in another? I'd think surely so - you wouldn't all be working on a project that could become obsolete in a matter of years - but maybe there is instead some plan to do a mass rewriting of the library every few years to port it over!

[Henrik Böving]

Yes mathlib will switch to Lean 4
But dont worry we dont have any plans for a Lean 5 yet :D

The changes are definitely breaking, we are currently working on a tool to auto translate mathlib called mathport though, the main issue holding us up right now is that not all tactics in Lean 3 are ported to Lean 4, yet and since tactic writing is drastically different in Lean 4 (in a better way though I'd claim :p) this cannot be automated.

[Will Fourie]

Interesting, do you know how long this rewrite project might take? I suppose that I have my lean 3 and mathlib copy on my computer, so I can keep using that even after the migration until I finish a particular project

Are the changes always like this? Just feels like it could be increasingly unwieldy the bigger the library gets.

How are the changes an improvement, out of curiosity?

[Johan Commelin]

Will Fourie said:

Are the changes always like this?

It's basically the first time this has happened. Bumps from Lean 3.x to Lean 3.y do not require such a large project.