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.

▲

derdi 10 days ago | parent [-]

> 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.

▲

SilasX 8 days ago | parent [-]

>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.

	▲	derdi 6 days ago \| parent [-]
		Gotcha. I've never had a problem with this usage. I guess I see the objection of "the goal is to prove the theorem" vs. "the (initial) goal is the theorem". It strikes me as overly pedantic, but we're talking about formal methods, so I guess pedanticism is warranted. I do want to note that systems usually use terms like "current goal" or "active goal", which do imply a sense of progress. I never felt that they imply that the current goal is a brand-new thing. It's a transformed version of the previous goal, hopefully made up of simpler parts that eventually become so simple as to be trivial, which then completes the overall proof.