Gamifying mathematics (an interactive tutorial for sequent calculus)

[ezyang]

http://logitext.ezyang.scripts.mit.edu/logitext.fcgi/tutorial?

[haliax]

The linked book by Pierce is pretty fantastic as well. http://www.cis.upenn.edu/~bcpierce/sf/

[rprospero]

I've been working on a similar project for high school algebra. Mine isn't as far along, so it's been nice to see some validation on my ideas, as well as get some thoughts on how I would improve.

[fusiongyro]

How do you make contraction happen? I don't see a button for it.

[ezyang → fusiongyro]

We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.