The main issue with Lean 4 is that there is currently no tactic state, but the designer Leo de Moura is currently hard at work at this, because they need tactics to start work on their IMO Grand Challenge https://imo-grand-challenge.github.io/ . Even when tactics are done, there will be no type class inference so the port of the maths library from Lean 3 to Lean 4 will probably not begin then. Type class inference is a complex issue and some of the chat on the zulip chat is about issues that users have been having in Lean 3 and how they might be fixed in Lean 4. But, in short, the basic principles are all the same. In short, I would thoroughly recommend this book.

Lean 4 has already gone public: https://github.com/leanprover/lean4/

Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.