Why learn Lean as written in the book when there is no way of knowing how much of it will be obsolete in Lean 4, which is being developed in private?
Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lean 4.
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.