Will Lean4 always be “Lean4”

Stream: lean4

[crab]

Will Lean4 always stay “Lean4”, or will it standardize into “Lean”? As Lean and Lean4 are treated as entirely different languages.

[Arthur Paulino]

I suspect it will just be "Lean" at some point, just like Python 3 became the standard for "Python"

[Patrick Massot]

I don't know for sure the answer to this interesting question, but the preceding case of transitioning from Lean 2 to Lean 3 suggests that the name will converge to Lean. In the mean time we are encouraged to write "Lean 4", not "Lean4".