lean4 install problems

Stream: lean4

[Quinn Culver]

Aloha, I'm trying to install lean4, on my Ubuntu, but can't even get

max_eq_right (nat.zero_le m)

[Mario Carneiro]

those are lean 3 mathlib theorem names, did you want lean 3 or lean 4?

[Quinn Culver]

Oh

[Quinn Culver]

Lean 4 is what I want

[Quinn Culver]

I think it's what I have.

[Mario Carneiro]

If you are doing mathematics then you should probably stick to lean 3 for the present, unless you like to live on the edge

[Quinn Culver]

well, even though I do like to live on the edge (was in a cave with 4 sharks last weekend)

[Quinn Culver]

I'm still gonna go for lean 3.

[Quinn Culver]

thanks