500 award if I start with your suggestion instead of lean, ~25 award if I find your comment interesting (adjusted for spam / answers posted just to get M$)
Bounty isn't 500 already because I think lean probably is the right choice so I don't want to potentially lock up 500 indefinitely
I'm a little bit interested in formalizing math stuff, but mostly just want to learn something new.
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.