Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lea

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/ https://github.com/leanprover/lean4/ Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.