question about the future of lean 3

Stream: general

[Gun Pinyo]

Lean 3 is still the recommend version of lean, due to fact that lean 4 is still under the development.
I am sure that lean 4 will bring many improvements over lean 3. However, once lean 4 is official released. Is the lean 3 still being maintain?

I am asking this because someone might still want to use lean 3 because of legacy reason or syntax convention (I like snake case more, easier to read).
I know this is lame, but sorry the camel case really sore and confuse my eyes. Anyway, I also would like to ask why lean 4 changes the naming convention from snake case to camel case? Is it because of fewer space required?

[Kevin Buzzard]

Probably the future of lean 3 will depend very much on how quickly the community is able to bring lean 4 up to the level of lean 3. Whilst some of us are optimistic that this process will happen quickly, in practice we just have to wait and see.

[Kevin Buzzard]

By up to the level, I personally mean how quickly we can get the maths library up and running. By the time it becomes feasible to do mathematics like manifolds in lean 4 in a nice and natural way, I can't imagine there will be much enthusiasm for supporting lean 3

[Kevin Buzzard]

But how long this will take is right now anybody's guess

[Scott Morrison]

weveGotOurWorkCutOutForUs