[jbapple]

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?

[kevinzz]

Lean 4 is no longer being developed in private; this was true a year ago but is no longer true. What is true is that Lean 4 is still not ready for the port of the maths library to begin, and we do not know when it will be. Furthermore, one cannot yet use Lean 4 within VS Code, which makes it more inconvenient to use than Lean 3. But we can wait. Lean 3 is good enough to do a lot of modern mathematics so it seems, and the community are happy to work with Lean 3 currently.

[mafribe]

How would you compare the state of proof automation to be expected from Lean 4 in comparison with Isabelle/HOL? I'm quite familiar with the latter.