Hello, I am from the Lean community, but I have a bit of experience with other provers too. I think you should absolutely start with Lean, for a few reasons:

• The Natural Number Game is a fun, game-like introduction to formalizing math.

• The Lean Zulip instance is full of lean users willing to answer questions and provide support. Other provers have forums as well, but they seem smaller and less beginner-friendly to me.

• Lean is math-focused, with a big math library, so that's a good match.

• My sense is that Lean has the best editor integration, in the form of its VSCode extension.

If there is a specific other prover you are thinking about, I'm happy to provide my perspective, if I've used it before.

Coq has a nice textbook(.Software Foundations (upenn.edu) ), associated books(https://www.penguinrandomhouse.com/books/656967/certified-programming-with-dependent-types-by-adam-chlipala), has been used for some large-scale projects like a formally verified C compiler, formal proofs of mathematical theorems like the 4-color theorem and Feit-Thompson theorem, and I think tools like Proof General for interactively viewing your proof contexts as you make steps in your proof were easier to use than Lean's.

I tried Lean4, but never did any serious work in either Lean or Coq. I know it uses the same underlying "Calculus of Constructions", so I would imagine it's equivalent to Coq and anything you learn you could transfer over pretty easily. And having these educational resources available might help more than using a newer surface language.

I think the main appeal of Lean would be if you want to contribute to the mathlib project specifically. And then you'd use Lean3.

Yes