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
   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.
Mark Reid October 19, 2007 Canberra, Australia
Subscribe: Atom Feed