There was a nice educational game for mobile devices called Dragonbox Elements that also did this, in a very kid-friendly way. But I always thought Dragonbox's

There was a nice educational game for mobile devices called Dragonbox Elements that also did this, in a very kid-friendly way. But I always thought Dragonbox's interfaces (they had an algebra game too) were almost too nice for kids' games, I wanted something more useful as a proof assistant. So very happy someone is exploring this space further! logitext.mit.edu/tutorial was also something similar, an interactive, puzzle-game like interface for proving statements in the sequent calculus. Maybe that can be an inspiration too?