Lean 5

Stream: lean4

[Tchsurvives]

Hi, just curious about the future of lean, are there still major unresolved issues that might require a future version and an accompanying migration of mathlib4? Or is mathlib4 the "final" mathlib version. Also wondering what's lean 4's type theory foundation, is it fixed? or could it change in future

[Mario Carneiro]

Lean 5 is not on the roadmap, and I don't think we have found anything that would require another rearchitecting. It is too early to really even begin to see what that would be, as lean 4 is still malleable enough that it adapts to fit our current needs. Maybe 3 years down the line we will have a better sense for whether lean 5 is coming, but right now it isn't even on the horizon.

[Mario Carneiro]

Mathlib doesn't really have versions, it moves fairly fast and is revised regularly. What you are seeing now is not really a new version of mathlib so much as a port of the existing library to a new lean.

[Mario Carneiro]

As for lean's type theory, it has not really changed between lean 3 and lean 4, and indications are that it is settling down (it was more configurable in the lean 2 days than it is now). I think we will see more embedded languages in lean 4 as a way of accommodating other logics, rather than a change to the type theory itself.

[Tchsurvives]

cool! wow i actually just came across your master thesis on "Type Theory of Lean" @Mario Carneiro thanks for the detailed explanation!