Proof Style
March 22nd, 2008 by WaltWhat makes a well-written proof? Who writes proofs well? Discussions of mathematical exposition usually revolve around larger-scale questions, such as how to organize the material, what kinds of examples to use, or how much background is necessary; by and large, around the question of what to put between the proofs. There is the art of choosing a proof, which is a subjective measure of taste. But once you’ve chosen the proof, what’s the best way to lay it out?
The style of my own proofs tends towards alternating sentences that begin with “Let” and sentences that begin with “Thus”.
March 22nd, 2008 at 10:59 pm
Hmm, after the introduction (which often contains “it suffices to show,” “define,” and “we will”), my proofs generally consist of paragraphs starting with “we note that”/”we see that,” “suppose toward contradiction that,” and “now, consider.” “Thus” happens in the middle of paragraphs as I explain logical steps, and also starts the conclusion paragraph.
I think more pertinent to making a clear proof, perhaps, is the use of terminology and concepts. For example, in my recursion theory proofs, I can obfuscate things with rigor by giving an (almost) explicit formulation of the algorithm in terms of recursive functions, or I can just appeal to the Church–Turing thesis and give a short description with words.
Another recent example: I’m constructing a function by stages. At each stage, I put some values in a bucket, and refer to previously-bucketed values when deciding what the output of this stage should be. Informally, I could use phrases like “add x to the bucket” or “the least y that hasn’t already been bucketed.” Or I could be more formal, and define a collection C_n for each stage n, so that “add x to the bucket” becomes “define C_n = C_(n - 1) U {x}” and “the least y that hasn’t already been bucketed” becomes “the least y \not\in C_(n - 1).” The former style is helpful if you already know what’s going on, and understand the purpose of the bucket and what it _should_ be filled with at each stage. But the latter style is clearer for grasping exactly what the algorithmic process is, without ambiguity. Which is “better” probably is rather dependent on the audience… personally, I’ve preferred the more formal style since, when doing homework, the whole point is to make sure that _I_ understand 100%.
A fun topic; hope my examples weren’t too rambling!
March 23rd, 2008 at 7:48 am
There’s a paper by Lamport about proof style, in which he argues that proofs should be structured hierarchically, so that one can find easily whichever level of detail you are at that moment considering:
http://research.microsoft.com/users/lamport/pubs/pubs.html#lamport-how-to-write
March 23rd, 2008 at 8:27 am
I think one of the biggest issues is the choice of the correct forest/trees ratio. How detailed do you make certain steps, where can you simply write “clearly” and “obviously”.
I also think it is important to have a linear sequence.:
Bad: X is blah blah, where X is defined to be Y.
Good: Define X to be Y. X is blah blah.
A violation of this is IMHO very confusing.
Just my 2c
March 23rd, 2008 at 10:45 am
Domenic: I think I would find the term “bucketed” or “bucket” confusing in a proof. In what field are these standard terms? How do they differ from sets? I know they were certainly never mentioned once in my recursion theory course. I think that very small terminology problems like this are one of the main causes of trouble reading proofs for me.
I don’t have much positive advice, though many an “obviously” or “clearly” has resulted in hours of “why on earth is this clear?” In general, I don’t like those words in proofs. If something is actually obvious, just state it. If you don’t want to work out the details, give a hint as to where you would start to. Remember, you may have been working on these problems for months, so what’s clear to you is different from what’s clear to your readers (especially graduate students like me).
March 23rd, 2008 at 11:47 am
Lucas: Bucketed is not standard terminology, no. But that’s part of the problem—the only real way to describe it accurately is “added to the mutable set X,” which ruins the whole idea of shorthand.
March 23rd, 2008 at 5:39 pm
I see the need for two kinds of proofs: one to establish the truth of a claim, and another to enlighten the reader. The former should be tediously detailed, with a computer program-like structure. The latter should emphasize motivation, intuition, and analogy.
I recommend Leslie Lamport’s article “How to write a proof.” http://research.microsoft.com/users/lamport/pubs/pubs.html#lamport-how-to-write
March 24th, 2008 at 12:59 am
I looked at the Lamport paper. I have to admit I fall into his “skimmers” group.
(BTW, Alex’s comment was in moderation when John posted his link.)
March 24th, 2008 at 2:03 am
For me, the most interesting idea in Lamport’s paper is…
“The ideal tool for reading a structured proof would be a computer-based
hypertext system.”
Maybe there’s hope that one day the referential advantages of the internet will play a more intrinsic role in the presentation of mathematics than floating pre-prints on arXiv.
March 25th, 2008 at 8:41 am
I think Lamport makes a great contribution to verification of theorems, but I don’t think his approach is enough for pegagogy. The two are not unrelated, and his approach would help readers drill into their desired level of detail. But there’s still the need for proofs that convey understanding. The popular approach of preceeding a proof with a list of unmotivated lemmas may establish correctness but obscure understanding. Maybe if there were more published Lamport-style proofs, professors would feel more freedom to talk about motivation, technique, and application, asking students to study the detailed proof for homework.
March 25th, 2008 at 6:24 pm
Actually, I’ve long had a pipe dream similar to Lamport’s idea, but more for explanatory or pedagogical reasons than ensuring formal correctness: have an e-paper or math blog where proofs of interesting results were short, snappy, and high-level, but where stages of the proof could be hyperlinked to fuller explanations for those readers who found the top stages too terse. I imagine tree structures similar to Lamport’s, but my idea would be to try to keep even the “lower” levels chatty and informal — to me his own examples verge on being mind-numbingly formal.
As an aside: I wonder where he gets the estimate “one in three papers has serious errors in it”. If most such errors go undetected (as he appears to suggest), it would seem that large amounts of mathematics would very quickly be in danger of total collapse. My own sense is that informal mathematical reasoning as traditionally presented is much more robust than he suggests — specialists in a field tend to know where to place their attention in checking the soundness of an argument, and the high connectivity of mathematics adds extra insurance against error.
On writing proofs, and in particular teaching students to write proofs: there are some interesting remarks on natural deduction and proof boxes, and their transcription into the more informal vernacular used by mathematicians, in chapter 1 of Paul Taylor’s book Practical Foundations of Mathematics.
March 25th, 2008 at 7:27 pm
“The popular approach of preceeding a proof with a list of unmotivated lemmas may establish correctness but obscure understanding.”
I’m not sure what you mean by this. Lemmas often improve understanding of a proof, or certainly make understanding of them more efficient, by the encapsulation and removal of certain arguments that would otherwise interrupt or obstruct the general flow of the proof. However, I do not like indiscriminate use of lemmas or lemmas whose assertion is totally subsumed by the assertion of the proposition that it is intended to support.
March 26th, 2008 at 1:35 am
Walt’s approach sounds a lot like the classic forward proof method. It is surprisingly difficult to find good advice on proof writing. The most inspirational suggestions to me were from a couple of articles by Paul Halmos. In particular, the AMS book by Steenrod, Halmos, Schiffer,
Dieudonne called “How to write mathematics” has several concrete suggestions. A nice summary of some of the key points can be found at: http://web.mit.edu/jrickert/www/mathadvice.html
March 26th, 2008 at 12:33 pm
Richard: I think the emphasis in John’s comment was on “preceding”. Lamport’s proof style is very lemma-centric, but the proofs of the lemmas appear as the lemmas are needed.
March 26th, 2008 at 3:50 pm
I think it is a common experience of people trying to formalize proofs so that they can be checked by a machine. Some errors are really hard to spot if you write your proof in English prose. Also the standards for correctness change when you have experience with theorem provers. Things like implicit use of the axiom of choice or referring to a variable bound by a quantifier outside of scope of that quantifier become serious errors.
And now a plug: for an example implementation of Lamport’s ideas on presenting structured formalized proofs, see http://formalmath.tiddlyspot.com .
March 26th, 2008 at 8:32 pm
Why are we not in bigger trouble if one in three papers has serious errors? If the conclusion is correct but the proof is flawed, that’s not a disaster. And if an incorrect result is so obscure that no one else is building on it, that’s not a disaster either. The worst case is a convincing but incorrect proof of a false result in the mainstream of mathematics that goes undetected. Those are quite rare. See Mark Dominus’s article along these lines http://blog.plover.com/math/major-screwups.html .
March 27th, 2008 at 5:10 am
I wonder where he gets the estimate “one in three papers has serious errors in it”. If most such errors go undetected (as he appears to suggest), it would seem that large amounts of mathematics would very quickly be in danger of total collapse. My own sense is that informal mathematical reasoning as traditionally presented is much more robust than he suggests — specialists in a field tend to know where to place their attention in checking the soundness of an argument, and the high connectivity of mathematics adds extra insurance against error.
I am confident that he believes this only because of the field he is in. Lamport does a lot of work in things like verifying protocols for asynchronous distributed systems. This area is full of intuitive arguments that sound appealing but turn out to be unformalizable or even false. If you don’t write your proofs very carefully, you will make mistakes, and nobody has the intuition needed to identify the mistakes without writing out formal details. I’ve talked with Lamport about this issue, and he just doesn’t realize that most of mathematics isn’t like that. He’s convinced that it’s wishful thinking on the part of mathematicians, and that much of mathematics is fundamentally flawed.
The one and only interesting example he has is the proof of the Schroeder-Bernstein theorem in Kelley’s general topology book. It sounds convincing, but the construction is stated wrong and doesn’t work. Of course, it’s just a small perturbation of a correct construction. From Lamport’s perspective, this shows how hard it is to find mistakes in casually written proofs. From mine, it shows the error-correcting nature of conceptual mathematics.
March 27th, 2008 at 11:32 am
Todd, although the proofs aren’t all exactly terse, there’s some major hyperlinking at the Fermat’s Last Theorem blog. You can click all the way back to the most basic levels of explanation.
March 27th, 2008 at 3:24 pm
Slawekk, I’ll bet you’re right — that’s probably the kind of thing Lamport had in mind.
John, those are good points, but I think before one can make any real sense of Lamport’s statistic, one has to get a good understanding of what he means by “serious” (cf. Slawekk’s comment). By the way, I got a “File Not Found” when I clicked on your link.
Jason, thanks for the reference. I’d like to see other attempts in this direction, with more in the way of conceptual explanations than what I saw on that blog (admittedly, I didn’t spend too much time looking at it).
March 27th, 2008 at 6:50 pm
I fixed the link in John Cook’s comment. It was Wordpress’s fault.
March 28th, 2008 at 5:09 pm
[...] of Style There’s an interesting discussion going on over at Ars Mathematica about proof styles, beginning with the question, “What makes a well-written proof?” I don’t have a [...]
March 29th, 2008 at 3:30 pm
Anonymous, thanks, that’s very interesting! And it confirms what I think Slawekk was suggesting.
Speaking of Schroeder-Bernstein: most of the proofs I’ve seen are fussy and aesthetically unappealing to me. I prefer a more abstract proof as follows: suppose that f: X –> Y and g: Y –> X are injective. Let PX denote the power set of X. Define a monotone function PX –> PX which sends a subset S of X to not g(not f(S)), where “not” denotes complementation. If this function has a fixed point T [i.e., if g(not f(T)) = not T], then we can define a bijection X –> Y which takes x to f(x) if x belongs to T, and x to g^{-1}(x) if x belongs to not(T).
Lemma: Any monotone function h: PX –> PX has a fixed point T.
Proof: Let T be the intersection of the set {S in PX: h(S)
March 29th, 2008 at 3:37 pm
Bah. Walt, could you fix this please? The remainder should have read:
Proof: Let T be the intersection of the set $latex \{S \in PX: S \subseteq h(S)\}$. Since h is monotone, $latex h(T) \subseteq h(S) \subseteq S$ for every $latex S$ in this set, and therefore $latex h(T) \subseteq T$. Applying the monotone function h again, $latex h h(T) \subseteq h(T)$. It follows that $latex h(T)$ belongs to this set, and therefore $latex T \subseteq h(T)$. Hence $latex T = h(T)$.
March 30th, 2008 at 2:34 pm
Anonymous, thanks, that’s very interesting! And it confirms what I think Slawekk was suggesting.
Actually, I meant something a little different. I read Slawekk’s comment as dealing with the ease of formal verifiability by computers, but Lamport’s worked up about a different issue (he doesn’t work on computer verification). In his work with asynchronous distributed systems, things can get extremely subtle and counterintuitive. It’s easy to come up with a protocol that sounds like it should work, and even to find a compelling argument for why it should work, when the protocol is inherently defective. If you’re unlucky, the proof will sound good enough that you’re sure formalizing it is merely a matter of writing down a few trivial details. Such “proofs” often get published in this area. The problem is that the objects of study are tremendously complicated and frequently pathological. Plus, the details are crucial: it’s not enough to convince yourself that there exists a protocol that probably works; instead, you want to know whether this particular protocol definitely works.
Most of conceptual mathematics is quite different. There are certainly many subtleties and some pathologies, but there’s a lot of intuition underlying most of mathematics, and mathematicians have spent the last couple of centuries working hard to develop a powerful intuition about the subtleties (quantifying ordering as in uniform continuity, etc.). I don’t know whether this is even possible in Lamport’s area, but it hasn’t been done yet.
So, basically, Lamport honestly believes mainstream mathematicians regularly prove false theorems using techniques that simply cannot be made to work, and he believes this happens on all levels (not just for unimportant theorems in obscure journals nobody reads, but for major, famous theorems). In his view, if we carefully wrote out our work using two-column proofs, we’d find irreparable logical errors in about a third of our proofs. I’m convinced he’s nuts, at least as far as this opinion goes, and he’s convinced that mathematicians are deluding themselves and unwilling to risk trying this project.
March 30th, 2008 at 6:08 pm
Anonymous — thanks for the clarification. Wow.
April 8th, 2008 at 10:08 pm
Anonymous: Wouldn’t it be more labor-efficient to develope better virtual testing for hyper-complex asynchronous protocols and forget about “proving” what works?
(The captcha words for this post were “Mr Scientist,” so I had to write something suitably Baconian.)
May 6th, 2008 at 8:41 am
Proofs and art have a lot in common. The old masters guide contemporary art. For polish and beauty I recommend Grundlagen der Analysis by Edmund Lanudau. Any mathematician can improve their proofs by trying to reach the standards he set in this timeless work.