Why is lean major version changing rapidly?

Stream: new members

[Julin S]

Is lean4 backward compatible with lean3 (I guess not? Since otherwise they wouldn't have changed the version number)? Why is the transition happening? Don't know if I'm wrong, but I got the feeling that lean is making too many backward incompatible changes.

First version appeared in 2012 (or 2013?) and by 2022 it's already on its 4th iteration.

I'm totally new to lean (have worked a little bit with coq before).

[Johan Commelin]

I think it's fair to classify the first versions of Lean as research projects. There never was a promise of long term support or backwards compatibility.

[Julin S]

Okay. That figures. Research is the main motive.

[Henrik Böving]

Also even Lean 4 is in itself making breaking changes rather often, e.g. when we removed auto Id.run or auto pure, Lean 4 code that's from the end of last year might very well not compile anymore with the current lean 4 nightly compiler

[Henrik Böving]

(wich is due to the fact Lean 4 does not have a final release yet though, everyone is just using nightly)

[Kevin Buzzard]

@Julin S we are not scared to make breaking changes. The community has learnt a great deal from mathematician users; the Lean developers have reacted to the issues which have arisen from making a huge monolithic mathematics library. They have also realised that the more lean is written in lean, the better. The language is still evolving. Lean 3 was very slow at certain things. Switching to lean 4 was a chance to fix these things. I don't know if I ever said this publically but Leo explicitly told me in around 2019 that it was too early to make a large mathematics library for Lean and I told him that we were having too much fun to stop now. He could foresee the problems we now have with the transition. But the community fully believes that it is powerful enough to work together and solve them, and then lean 3 will be consigned to history. Lean is still a project, not a product. A lot of what is happening is very experimental -- for example nobody had tried to formalise much of the mathematics we're formalising now, in any theorem prover. Yet I am not naive enough to believe that just because Lean 3 has taken us so far that it is the perfect system. I trust the developers to know what they're doing; they wanted to rip everything up and start again to solve various problems they could see and who am I as a user to say this is bad idea. Most lean 3 code is mathematics and the vast majority of the important stuff will be ported, mostly automatically. The community is brave to take this on but we believe we're doing the right thing.