I do like this stuff. It reminds me of Terrence Tao's QED game. I would like if you would be able to undo a part of a tree, rather than just in general.
Thanks. Yeah, I remember playing through QED when I researched competition. It was a good game but didn't match my Advanced Graphics :)
Undoing a whole subtree sounds like a good idea, especially for the future first order version where proof trees are likely bigger.
