Table of Contents
Preface
On March 15, 2006, Leslie Lamport gave a public lecture called How to Write a Proof at the University of Lugano. This note is my account of the event.
As you read the paragraphs below, keep in mind that they are based on my handwritten notes, rather than a word-for-word transcript of the lecture, and that they reflect my impressions and my recollection of what he said.
Content
Abstract
How to Write a Proof was a talk that proposed an approach to writing proofs that requires the refactoring of the proof into very short sub-proofs, each containing perhaps three steps; the result of this procedure is what Dr. Lamport calls a structured proof. The process can seem daunting and can, indeed, be time-consuming, but it leads to proofs that are easier to read and, therefore, to proofs that are more likely to be correct.
Making Proofs Easier to Write Read
Most mathematicians wish to make proofs easier to write, but Dr. Lamport wants to make proofs harder to write — but only because this is what it will take, he claims, to make proofs easier to read. The primary motivation for such an undertaking is that approximately one-third of all published proofs have serious errors, even after peer-review; therefore, making proofs easier to read should take precedence over making proofs easier to write.
Prose
Hundreds of years ago, proofs were written in prose. At around the time of Newton, symbols and formulas make their way into proofs, but the transition is incomplete and, in fact, proofs written in the twentieth century feature lots of prose. This is unfortunate because prose remains, demonstrably, a source of error in proofs: in trying to make the prose easier to read, important details may be glossed over and, as a consequence, the foundations of the proof endangered. Prose, says Dr. Lamport, encourages mathematicians to “throw out the baby with the bath water” — or, at least, makes doing so very appealing. Someone said that a proof should be great literature, and prose-prone mathematicians seem to agree, but Dr. Lamport begs to differ: he says that proofs should be great art, and that this does not require prose because the beauty of a proof lies in its logic.
Formulas
Formulas are actually easier to read than prose. This is obvious to anyone who has to work with them. There are many reasons for this:
- Formulas are shorter.
- Formulas give names to the main actors in a proof.
- Formulas have a visual structure.
As Professor Pedone has said, reasoning-by-prose is best put to use in convincing oneself of what one has already found to be true.
Proofs Using Formulas
A simple form of the aforementioned approach (stating steps as formulas and writing justifications/comments alongside as needed) yields a proof that may look like this:
| Hypothesis: "dynamic" math is dumb. | |
|---|---|
| Step | Justification |
| x = x | Aristotle said so |
| QED | |
While this works well for very short proofs involving only sequence, it is less than elegant for long proofs the statements of which have dependencies that form a hierarchy.
Structured Proofs
The alternative to, or refinement of, the aforementioned style of proof is a hierarchically numbered proof that takes a high-level proof that may look like this:
and fleshes it out with lower levels that look like this:
As a structured proof grows longer, it becomes necessary to resort to special notation described in How to Write a Proof (whence all of the beautifully typeset figures appearing in this note were taken) in order for the labels to remain shorter than the statements. The impact of this device can be appreciated in the following figure:
How deeply should statements be nested? This depends on factors like necessity, novelty, and even the intended audience. In any case, it should contain no long paragraphs, and should be finely grained. Dr. Lamport has observed that the probability that one makes a mistake while writing a structured proof decreases exponentially with the number of levels, so getting carried away with this method can only help you. :-) Actually, the real challenge is fighting off laziness.
Pros and Cons
The structured-proof approach makes proofs easier to read. This feature makes a structured proof easier to check, which makes it harder to publish incorrect results accidentally. Additionally, resuming work on a structured proof is easier because the required mental context is easier to bootstrap, which means that structured proofs are easier to maintain, too.
Unfortunately for some people, because structured proofs are easier to pick apart, it is a lot harder to get one published when it's wrong; that is, structured proofs make it harder to publish incorrect results “accidentally on purpose”. OK, so this isn't a con, after all.
Structured proofs do, however, suffer from one shortcoming: on paper, at least, the structure of long proofs is hard to see. Dr. Lamport says that rendering the proofs as a hypertext ought to solve this problem, though.
Form
The Good
As on the previous day's lecture, Dr. Lamport spoke audibly and intelligibly. The pace was adequate for the audience, which included many non-technical people. Although the base knowledge assumed of the audience was minimal, he did occasionally wink in our general direction, as in the case of the slide featuring a statement of Fermat's Last Theorem in prose. Entertaining anecdotes motivated and illustrated points well. He spared his audience the technical wink-wink, nudge-nudge anecdotes to which we, undergraduates, had been treated on the previous day.
The Bad
Some of the slides featuring proofs or parts thereof were very plain and very “busy” (very much in the style of mathematicians, I suppose) and probably terrified a good part of the audience, which included spouses of faculty members and SO's of students, not all of whom were technically inclined. One can hardly fault professor Lamport for this, though: if he hadn't shown these slides I would have been upset! :-)
It was a great pity (for me) that the Q&A session, which could have been even more interesting, was cut somewhat short by Dean Jazayeri, who (ever the thoughtful host) must have realized that the schedule was slipping and that people were eager to get some face-to-face time with the visiting celebrity before going home.
The Ugly
Someone in the audience may have embarrassed himself by asking a question that could easily have been construed as the sort of question intended to show how much one knows but which, generally, accomplishes the opposite. I could be wrong, though; indeed, he seemed unabashed by the exchange and tried again during the apéro.
Summary
Dr. Lamport presented the material in a low-glitz style, as on the previous day, and obtained the same result as on the previous day: mathematically-inclined people were spell-bound (and, I daresay, sold on structured proofs) and mathematically-disinclined people were… in awe of Dr. Lamport's mad math-fu. ;-)
Seriously, though, several notions presented in this lecture are widely applicable and were, I think, accessible to all present. If you are interested in structured proofs or even just in the general notions underlying Dr. Lamport's approach to writing proofs, you ought to read the original paper.