Some quick info for Lean:
Homepage: https://leanprover.github.io/
Source: https://github.com/leanprover/lean4
Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)
The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4
Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4 blazingly fast https://leanprover.github.io/publications/
Galois inc reproduced benchmarks by the Lean 4 devs that show that Lean 4 regularly outperforms the C++ stdlib.
This is an awesome mix of raw speed, functional programming, and formal software verification.
For people interested in using Lean, note that there's a community fork (https://github.com/leanprover-community/lean) of the last official Lean 3 release 3.4.2 (https://github.com/leanprover/lean). The fork is still under active maintenance, so might be a better place to start (the main development team have moved onto developing Lean 4.0 (https://github.com/leanprover/lean4), and it's not clear when that will be ready).
Lean 4 WIP is public now: https://github.com/leanprover/lean4. But PRs aren't welcome. Personally I think Coq's done waaay better at community management.
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.
Where can I read more about the decision to develop Lean 4 in private, and what is the status of https://github.com/leanprover/lean4, in your view?