Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between th

Re Lean 3/4 problems: the port of mathlib from Lean 3 to Lean 4 just finished this summer, and unfortunately there's still going to be some confusion between the two for a little while! The mathlib community has been working on getting the documentation to all refer to Lean 4 -- if you find anything old please point it out on the Zulip. There's usually someone around who can fix it relatively quickly. I think it's better to think of it as bleeding-edge research software rather than alpha software. There might be a little bit of culture shock if you're used to industry-oriented software, but part of this stable version announcement is that there's a new Lean organization that now has resources to improve the experience.