lean 5

Stream: general

[Dean Young]

Will there ever be a lean 5? Will it be compatible with Lean 4?

[Alex J. Best]

From what I recall of this question being asked to the devs, there are no plans for a Lean 5 to exist, especially given the huge redesign that lean 4 represents over lean 3, and how extensible lean 4 is. So there is no way to answer the second part of the question really

[Ruben Van de Velde]

I'd hope lean 5 comes with a fully automated porting tool!

[Martin Dvořák]

I'd hope lean 5 comes with a fully automated theorem prover!

[Dean Young]

I hope it comes with Kullback Leibler divergence tools for exponential distributions on Mathlib.