# The Mathematical Grue

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

> 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

that it was probably proven in the 50s by a Russian.

> s

You sit back down at your desk and spend half an hour

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,
Your theorem was eaten by a Grue.