There’s a certain class of computer games out there, sometimes characterised as 4X games (“eXplore”, “eXpand”, “eXploit” and “eXterminate” or some such), that are known for their addictive “just one more turn” qualities. The first game in this mold was probably Civilisation, where the player has to control a civilisation from its earliest beginnings all the way to the point where it is ready to send a space-ship to Alpha Centauri. (This PC game has only a very tenuous connection to the classic board-game of the same name.)

I’d just like to briefly claim that interactive theorem-proving is
subject to a similar phenomenon, which I (and others) call “just one
more lemma”. Say you’re trying to prove big complicated theorem
*X*. You spend a while on this before realising that you can’t
prove it, without first proving supporting lemma *Y*. But then
it becomes clear that *Y* needs a theorem about lists that the
developers of the system haven’t included (incredulously you think to
yourself, “How on earth could anyone ever prove anything without
first knowing that ```
MEM x (FILTER P l) = MEM x l /\ P
x
```

? I mean; come on!”)

These “to prove *X*, I will first need *Y*” links
build into ever larger stacks. In fact, it can become easy to lose
track of the original goal entirely. But now, I have to go and prove
sub-lemma *Z103*.

Comments