A discussion over at God Plays Dice had me nodding in agreement: proving a theorem is like playing an adventure game. As Isabel puts it
You are in a maze of twisty little equations, all alike
alluding to a particularly fiendish puzzle in the text adventure Colossal Cave.
Having recently grappled with some tricky proofs I was wondering how they might play out as a piece of interactive fiction…
You are sitting before a particularly thorny conjecture.
Possible proofs lead away from here in several directions.
> inventory
You are carrying the following items:
A ream of blank paper
A pencil
The Cauchy-Schwarz inequality
Some half-remembered undergraduate mathematics
> look conjecture
You stare blankly at the conjecture. You think it might
have something to do with convexity.
> w
You surf over to Wikipedia and read up on sub-tangents.
The notation makes you confused.
There is a lemma here.
> take lemma
Taken.
> e
You wander off to go get a bite to eat and some coffee.
You see a colleague here.
> talk colleague
After explaining your conjecture your colleague mutters
that it was probably proven in the 50s by a Russian.
> s
You sit back down at your desk and spend half an hour
reading pages linked to from reddit.
You see an unproved conjecture here.
> use lemma
[on the conjecture]
With a bit of manipulation you turn the equation into one
involving the expectation of a product.
> use Cauchy-Schwarz
[on the conjecture]
Hooray! You now have a tight bound on a key quantity,
proving your conjecture.
> generalise assumptions
Your theorem was eaten by a Grue.