32
$\begingroup$

Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.

I understand that a transition to Lean 4 is looming. I've heard that Lean has had issues with backwards compatibility in the past, but I don't know the details.

When is Lean 4 expected to become the most widely used version of Lean? Will mathlib suffer from this transition? If so, how?

$\endgroup$

1 Answer 1

36
$\begingroup$

BIG UPDATE

The port to Lean4 is officially complete. There is a couple changes that we are still hoping to officially put into mathlib3 before moving it into mathlib4, but the content in mathlib3 is now a strict subset of the content of mathlib4, apart from tactics. In the very near future, the mathlib3 repository will be frozen, and all future development should now be done in Lean 4. This does not mean that Lean 4 is stable yet - there is a lot of hard work right now into this.


The community hopes to eventually move fully to Lean4. There's some details about the history of earlier Lean versions here, but they're not too relevant as the first two versions were very experimental. Now, some members of the community and Microsoft are diligently working on mathport, which will hopefully provide a full syntax-ful translation of Lean3 code into idiomatic Lean4 code. The main test-case for this, at the moment, is mathlib itself, and we are pretty determined to make it work.

This blogpost offers some further details on what to expect from the transition - there's still not been a consensus on how gradual the transition is, but I suspect that eventually there will be a day declared where there is an announcement "no more PRs to mathlib3 will be accepted, please move your work over to Lean 4".

UPDATE (Jan '23): Currently, there's a "progressive locking" model going on, where we are porting files and, as soon as a file is ported to mathlib4, any PR to it in mathlib3 must be accompanied with an equivalent PR to mathlib4 making the same changes. About 20% of all files have been ported, and also many tactics (definitely over 20% of them!), but I do not think this means 20% of the work has been done - later files in the import hierarchy are often much harder to port (and also often longer).

UPDATE (Apr/May '23): We are now at 60% progress; this can be tracked here.

$\endgroup$
1
  • 3
    $\begingroup$ I think it would make sense to keep the previous parts of your answer, even if they are somewhat out of date, in particular the links to mathport and the blogpost. These are definitely of value to someone interested in the question of the Lean 3-to-4 transition, even if it is completed, and such a person might end up on this post through search engines. $\endgroup$ Jul 27, 2023 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.