I want to play around with proof assistants, currently thinking Lean. Should I start with something else?
No bounty left
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.
This question is managed and resolved by Manifold.
Get 
1,000 to start trading!
1,000People are also trading
Related questions
Will natural language based proof assistants be in common use by 2026?
25% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Frontier science theorem discovery fully formalized in proof assistant before 2028?
23% chance