[kevinzz]

There is every way of knowing how much will be obsolete in Lean 4, as long as you're following the discussions at https://leanprover.zulipchat.com . The type theory of Lean 4 will be the same as Lean 3, there are some minor syntax changes and conventions for variable naming have changed from this_way to ThatWay but all the type theory is the same and the book will be an excellent introduction to Lean 4.

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.