Lean essentially gamifies learning math and you always know if you got the right answer. Moreover, unlike written math which is rife with ambiguous notation (unless you’re an expert), math in a theorem prover like Lean is always unambiguous.
Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.
What about Lean made you decide to use it for this project? The Tactics system?
Lean is an interactive proof assistant, not an ATP. If you're actively using Lean (or for that matter any other proof assistant), you're definitely "learning how to make proofs". Induction-based proofs, specifically, are notoriously hard to automate.
A series of levels where you prove ever-more-complex theorems in Lean, gaining each proved theorem as a tool to use in proving further theorems! Best puzzle game I've played in years.
That's a very high bar, and not likely to be reachable for quite some time. The most worthwhile, reasonably short-term goal in formalized mathematics is "simply" to completely formalize some sizeable part of the undergrad curriculum. (One should note that a proof formalization is publishable work on its own, because the process of formalizing a proof in some given system does help clarify the underlying working of it in a way that's not obvious from an informal sketch.)
https://news.ycombinator.com/item?id=22390486
https://news.ycombinator.com/item?id=21200721
https://news.ycombinator.com/item?id=20909404
(These are links for the curious. I add that because readers sometimes assume that we're chiding people for posting related things. Pas du tout!)
