To me, what makes a game a game is that you can learn how it works simply by interacting with it; you don't need to open a separate wiki. That is not entirely true, as for examples fighting games have been infamous for needing to go online to learn how combos work, but this is widely considered to be a major factor of why the genre is unpopular, and recent games have tried to at least give proper tools (in training mode). Right now, it feels a bit like a series of exercises with the guiding text replaced by dungeon fluff; it's pretty neat, yet you could as much say 'just give me the tutorial'.

In a game format I would for instance expect not to have to type the "proof [...] qed" part for example; its purpose is to be a bounding box, but interacting through text is cumbersome -- it isn't really for a developer who sees the benefit of plain text, but it is for a most users who might bang their head against the syntactic impedance mismatch.

To put that into perspective though, I remember Brett Victor's "Alligator Eggs", and the idea is very compelling; games are self-motivating, so if you can learn some real skills then you solved everything. Combinatory logic, sequent calculi etc naturally lend themselves pretty well to the puzzle formats, yet I don't think there's anyone who really succeeded at any real implementation of it.

I'm mostly rambling my own view on the subject here, it's certainly an interesting experiment :-)