Comment by wging
3 days ago
There is a game already, though it may not be exactly what you want (and the goal is definitely not "generate all known math"). I've played around with it, and I do think it's pretty fun.
The article mentions it, in fact: https://adam.math.hhu.de/#/g/leanprover-community/nng4
How did I miss this! Thanks for pointing it out. This is scratching the itch.
Had a blast with that game, really scratched that puzzle itch, and got to relearn some long-forgotten knowledge.
I played through a lot of it, and while it was fun, I wouldn't call it gamified in the sense that Zachtronics does it. As an FYI, here are some sticking points I ran into as well:
1) It uses the term "goal" for the the current stage of the proof you're working on, which is counterintuitive. In common speech, the goal is the theorem you're trying to prove, not the current step you're on in proving it. It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
2) It doesn't warn you early on about the left-associativeness of the operator binding, or what to do about it. So you can apply what seem like valid transformations but then parentheses pop up that you don't expect, and which you have no guidance on how to deal with. I had to ask ChatGPT what was going on to solve it.
> It would be like if I were helping you get to work in the morning, and I said, "Okay, you're current [sub]goal is that you're done brushing your teeth." No. That's not a goal. That's progress toward a goal.
Interesting. Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work? And if we then do brush our teeth, wouldn't you say that the remaining goal is to get to work? In this scenario, if anything can be called progress, it is what's in the past (the showering etc.), not what is still to be done.
>Let's say our overall goal is to get to work showered, wearing clean clothes, and having brushed our teeth. After we showered and put on clean clothes, wouldn't you say that the remaining goal is to brush our teeth and get to work?
Yes, I agree! My issue is not with the reality of having reduced the problem to a different one, but with the "goal" metaphor, which is counterintuitive to how that term is normally used, especially since it connotes that each step is some brand new thing, rather than progress.
And sure, like any technical jargon, you can learn to accept some specialized term-of-art usage, but I'd prefer it be conducive to developing a correct ontology of what is going on in an assisted Lean proof.
While "subgoal" is better, I think the issue even goes back to calling the original theorem a "goal". Really, the goal is to prove the theorem. So a better term, more conducive to intuiting the Lean ontology, would be something like "[remaining] unresolved proof state", even though it's more verbose. (Perhaps you could get the best of both worlds with some kind of footnote for new users that clarifies that this is what "goal" means here.)
With that said, I appreciate the pushback, as your comment forced me to more carefully think about what I was objecting to.