Dear Meg,
In my last letter I told you why proofs are necessary. Now I turn to the other question I raised: what is a proof?
The earliest recorded proofs, along with the notion that proofs are necessary, occur in Euclid. His Elements, written around 300 BC, laid out much of Greek geometry in a logical sequence. It begins with two types of fundamental assumptions, which Euclid calls axioms and common notions. Both are basically a list of assumptions that will be made. For instance, axiom 4 states that “all right angles are equal,” and common notion 2 states that “if equals be added to equals, the wholes are equal.” The main difference is that the axioms are about geometric things and the common notions are about equality. The modern approach lumps them all together as axioms.
These assumptions are stated in order to provide a logical starting point. No attempt is made to prove them; they are the “rules of the game” for Euclidean geometry. You are free to disagree with the assumptions or invent new ones, if you wish; but if you do, you are playing a different game with different rules. All Euclid is trying to do is make the rules of his game explicit, so that the players know where they stand.
This is the axiomatic method, which remains in use today. Later mathematicians observed gaps in Euclid’s logic, unstated assumptions that should really be included as axioms. For example, any line passing through the center of a circle must meet its circumference if the line is extended sufficiently far. Some tried to prove Euclid’s most complex axiom, that parallel lines neither converge nor diverge from the others. Eventually, Euclid’s good taste was demonstrated when it was realized that all such attempts are bound to fail. To muddy the philosophical waters, over the centuries, various deep difficulties in the axiomatic approach have appeared, such as Gödel’s discovery that if mathematics is logically consistent, then we can never prove it to be so. We can live with Gödelian uncertainties if we have to, and we do have to.
Textbooks of mathematical logic base their descriptions of “proof” on Euclid’s model. A proof, they tell us, is a finite sequence of logical deductions that begins with either axioms or previously proved results and leads to a conclusion, known as a theorem. Provided each step obeys the rules of logical inference—which can be found in textbooks on elementary logic—then the theorem is proved.
If you dispute the axioms, you are also free to dispute the theorem. If you prefer alternative rules of inference, you are free to invent your own. The claim is only that with those rules of inference, acceptance of the stated axioms implies acceptance of the theorem. If you want to make π equal to 3, you have to accept that all numbers are equal. If you want different numbers to be different, you have to accept that π is not 3. What you can’t do is pick and mix, having π equal to 3 but zero different from one. It’s as simple and sensible as that.
This definition of “proof” is all very well, but it is rather like defining a symphony as “a sequence of notes of varying pitch and duration, beginning with the first note and ending with the last.” Something is missing. Moreover, hardly anybody ever writes a proof the way the logic books describe. In 1999 I was musing on this discrepancy, having accepted an invitation to a conference in Abisko, Sweden, on “Stories of Science and the Science of Stories.” Abisko is north of the Arctic Circle, in Lapland, and a group of about thirty science fiction writers, popular science writers, journalists, and historians of science were going to spend a week there seeking common ground. Wondering what I was going to say to them, I suddenly realized what a proof really is.
A proof is a story.
It is a story told by mathematicians to mathematicians, expressed in their common language. It has a beginning (the hypotheses) and an end (the conclusion), and it falls apart instantly if there are any logical gaps. Anything routine or obvious can safely be omitted, because the audience knows about such things and wants the narrator to get on with the main story line. If you were reading a spy novel and the hero was dangling above a chasm on the end of a burning rope hanging from a helicopter, you would not want to read ten pages on the force of gravity and the physiological effects of a high-velocity impact. You’d want to find out how he saves himself. It is the same with proofs. “Don’t waste time solving the quadratic, I know how to do that. But tell me, why do its solutions determine the stability of the limit cycle?”
In my paper (reprinted in Mission to Abisko) I said this: “If a proof is a story, then a memorable proof must tell a ripping yarn. What does that tell us about how to construct proofs? Not that we need a formal language in which every tiny detail can be checked algorithmically, but that the story line should come out clearly and strongly. It isn’t the syntax of the proof that needs improvement: it’s the semantics.” That is, the essence of a proof is not its “grammar” but its meaning.
In that paper, I contrasted this admittedly vague and woolly notion with a much more formal one, the idea of a “structured proof,” advocated by the computer scientist Leslie Lamport. Structured proofs make explicit every step in the logic, be it deep or trivial, clever or obvious. Lamport makes a strong case in favor of structured proofs as a teaching aid, and there’s no doubt that they can be very effective in making sure that students really do understand details. Part of that case is an anecdote: a famous result called the Schröder–Bernstein theorem. Georg Cantor had found a way to count how many members a set has, even when that set is infinite, using a generalized type of number that he called a “transfinite number.” The Schröder–Bernstein theorem tells us that if two transfinite numbers are less than or equal to each other, then they must actually be equal. Lamport was teaching a course based on the classic text General Topology by John Kelley, which includes a proof of the theorem, but when the extra details needed for the students were added, Kelley’s proof turned out to be wrong.
Years later, Lamport could no longer locate the error. The proof seemed obviously correct. But five minutes spent writing down a structured proof revealed the mistake again.
I was worried, because I’d put a proof of the Schröder–Bernstein theorem into one of my own texts. I looked up Kelley’s proof for myself but could not discover a mistake. So I e-mailed Lamport, who suggested that I write down a structured proof. Instead, I worked my way very systematically through Kelley’s argument, in effect creating a structured proof in an informal way, and eventually I spotted the error.
There is a classic proof of the Schröder–Bernstein theorem that starts with two sets, corresponding to the two transfinite cardinals. Each set is split into three pieces, using a notion of “ancestor” invented purely for this particular proof, and the pieces are matched. In effect, this proof tells a story about the two sets and their component pieces. It’s not the most gripping of stories, but it has a clear plot and a memorable punch line. Fortunately, I had used the classic proof in my textbook, and not Kelley’s reworking of it. Because Kelley had told the wrong story. Attempting, I suspect, to simplify the classic version, he had overdone things and violated Einstein’s dictum: “as simple as possible, but not more so.”
The presence of this mistake supports Lamport’s view about the value of structured proofs. But, to quote my paper, “There’s another interpretation, not contradictory but complementary, which is that Kelley told a good story badly. It’s rather as if he’d introduced the Three Musketeers as Pooh, Piglet, and Eeyore. Some parts of the story would [still] have made sense—their inseparable companionship, for instance—but others, such as the incessant swordplay, would not. . . .”
If we think of a proof in the textbook sense, all proofs are on the same footing, just as all pieces of music look like tadpoles sitting on a wire fence when expressed in musical notation, unless you are an expert and can “hear” sheet music in your head. But when we think of a proof as a story, there are good stories and bad ones, gripping tales and boring ones, like stirring or insipid music. There is an aesthetic of proof, so that a really good story can be a thing of beauty.
Paul Erd~s had an unorthodox line on the beauty of proofs. Erd~s was an eccentric and brilliant mathematician who collaborated with more people than anyone else on the planet; you can read his life story in Paul Hoffman’s The Man Who Loved Only Numbers. Anybody who coauthored a paper with him is said to have an “Erd~s number” of one. Their collaborators have Erd~s number two, and so on. It’s the mathematician’s version of the Oracle of Kevin Bacon, in which actors are linked to Bacon by their appearances in the same movies, or by their appearances with actors who’ve appeared with Bacon, and so on. My Erd~s number is three. I never collaborated with Erd~s, and I’m not on the list of people with Erd~s number two, but one of my collaborators is.
Anyway, Erd~s reckoned that in Heaven, God had a book that contained all the best proofs. If Erd~s was really impressed by a proof, he declared it to be from “The Book.” In his view, the mathematician’s job was to sneak a look over God’s shoulder and pass on the beauty of His creation to the rest of His creatures.
Erd~s’s deity’s Book is a book of stories. I ended my Abisko talk like this: “Psychologists now tell us that without emotional underpinnings, the rational part of our mind doesn’t work. It seems that we can only be rational about things if we have an emotional commitment to such a recently evolved technique as rationality . . . I don’t think I could get very emotional about a structured proof, however elegant. But when I can really feel the power of a mathematical story line, something happens in my mind that I can never forget . . . I’d rather we improved the storytelling of proofs, instead of dissecting them into bits that can be placed in stacks of file cards and sorted into order.”