Why We Need Structured Proofs in Mathematics

I argue about the advantages of using structured proofs (à la Leslie Lamport) in Mathematics, tell my personal experience with them, and offer suggestions on how you can start writing your own structured proofs.

Motivation

When mathematicians write a standard proof of some theorem, they have to decide on which level of detail they will present their argument. If they provide too little justification, readers may spend a lot of time filling the holes left or, even worse, may not understand why a specific step of the proof is correct. However, more argumentation isn’t necessarily always better, since this may obscure the “big picture” and some readers may be more interested in seeing the “big picture” than in checking every tiny detail of the proof.

The ideal level of detail in a mathematical proof varies from reader to reader, as it depends on the reader’s background and the reader’s intention (see the “big picture” and get an intuition vs check that every step of the proof is correct)!

Is there a way to satisfy every type of reader?
I believe that by using proof sketches, lemmas, and structured proofs it is possible to get really close to this ideal.

However, while the use of proof sketches and lemmas in the presentation of a mathematical result is common in the mathematical literature, structured proofs à la Leslie Lamport don’t get the attention they deserve.

What is a structured proof?

Structured proofs as an alternative style of writing proof are captivatingly described by Leslie Lamport in this article and this article. I strongly recommend reading them, as these two articles are among the best scientific articles I have ever read.

It’s better to illustrate structured proofs via an example, comparing them to normal proofs. This example comes from here and it’s about a corollary to the Mean Value Theorem, which is a theorem from calculus. Here is the corollary and the proof as presented in Spivak’s Calculus textbook:

An example of a standard non-structured proof.

And here is the correspondent structured proof presented by Leslie Lamport in the mentioned article:

The corresponding proof, presented in a structured manner.

Notice that it is easier for a reader to see the structure of the proof: what were the necessary steps and the justification for each one. The reader “A”, who (let’s say) already knows a lot of calculus, can just read steps 1–5 and be convinced that the proof works. A reader “B” that is studying calculus for the first time and wants to make sure he understands everything can read steps 1–5 to get the “big picture” and then understand each step by reading the proof for that step.

Ok, but imagine that a struggling reader “C” didn’t understand the justification of step 2. What can we do? We simply expand the justification of step 2 in a structured manner, as shown below (this also comes from the mentioned article):

Expanding the proof of step 2 in a structured way.

This way, readers “A”, “B” and “C” will all be satisfied! The reader “A” can just read the steps 1–5 as before. The reader “B” when reading step 2 may just read steps 2.1–2.3 (without reading the proof of each substep) and be convinced. And the struggling reader “C” will read all steps, substeps, and justifications and (hopefully) have no doubts.

If we used the conventional, non-structured way of writing proofs, we would not be able to please everyone, since everyone would be reading the proof in the same way and the level of detail wouldn’t satisfy “A” “B” and “C” simultaneously.

Advantages

1. As described before, by writing proofs in a structured way it is easier to add the necessary details that justify each step without “clouding” what are the main steps of the proof.
2. Writing proofs in a structured disciplined manner makes it harder to prove things that are not true! If you feel that a justification for a given step “S” is not good enough, you can break it down into substeps and carefully explain each substep until you are convinced that step “S” really holds. Additionally, the hierarchical way of the proof will make it easier to spot if you missed a corner case. Note that for this point to work it is not enough to just write a structured proof, but also fill every little hole in the proof.
3. If you send a paper to publication and write a structured proof as described in 2 it will make it easier for the reviewer to check if your demonstration is indeed correct.
4. Writing structured proofs is more fun than writing traditional proofs, in my opinion.

Disadvantages

1. Writing a proof in a structured way takes more space than writing in the standard way. If you’re writing a paper and you have a page limit, it may be better to leave the structured proof to an extended version of the paper, which you can make available online. If what you are publishing will be printed, then extra pages may mean killing extra trees which is bad.
2. Writing a carefully constructed structured proof takes more time than writing a sloppy proof with holes to fill for the reader. However, the difference in time between doing a carefully structured proof and a careful proof written in traditional style is not huge and it is worth the investment, in my opinion.

How can I start writing structured proofs?

Ok, if this is your first time reading about structured proofs, here what I would do if I were you. Since Leslie Lamport came with the concept, I would begin by reading his papers on the subject. They are available here and here.
When writing your next proof in LaTeX, just use the package pf2 which can be found here. Although there is a computer program called TLA+ described by Leslie in his papers, I would simply start with pf2 since I believe it is easier to use and sufficiently powerful for most tasks.

My background and personal experience with structured proofs

I am currently a Ph.D. student in computer science at the University of Brasilia (UnB-Brazil). In my research (for instance here), I use interactive theorem provers (I use PVS) to make sure that what I prove is indeed correct.

After discovering them last year, I have read about structured proofs and wondered when/if I would have the opportunity to play with them. I got my opportunity with the structured proofs à la Leslie Lamport when preparing a seminar for my class of type theory during this semester.

We used Hindley’s book “Basic Simple Type Theory” (this book here) and me and my classmate Francisca had to explain topics 8E and 8F of the book. We opted to present the proofs in a structured manner. You can find our slides here. I talked to some of my classmates and they liked the structured approach adopted, saying that the indentation helped clarify how the arguments fit together and that the presentation of the proofs was smooth.

Structured proofs vs Interactive Theorem Provers (ITPs)?

I think both structured proofs à la Leslie Lamport and interactive theorem provers (ITPs) are valuable tools. Structured proofs and interactive theorem provers should not be seen as rivals, but as different tools for different kind of situations.

When using interactive theorem provers, the computer checks every step of the proof so the chance of proving an incorrect result is drastically reduced, even more than if we used structured proofs and provided detail for every little step and substep.

However, structured proofs do have advantages over interactive theorem provers. For instance, it is easier to learn how to write structured proofs than how to use an ITP. Additionally, structured proofs (for instance the ones shown in this paper) are nicer to read than the ones obtained from an ITP. Also, proving things using an ITP, in my experience, is a lot slower than writing a structured proof.

I believe that structured proofs are a necessary tool in the toolbox of the mathematician of the 21st century. I am not so sure, however, if every mathematician needs to prove his theorems using an ITP… But that’s just my opinion.

Other nice posts about structured proofs

First and foremost we have Leslie Lamport’s article on the theme. They should be your main reference (and not this post). As mentioned before, they are available here and here. This post here is also nice. And Leslie gave a lecture about it, which is available here.

EDIT: This post gave rise to a paper about structured proofs. The extended version of the paper, the slides of the talk and the link to the video can be found here.

Conclusion

Structured proofs are a nicer way to present a demonstration than the current style of writing proofs in mathematics. If the writer maintains a discipline of providing detailed justification for each step, they also make it harder to prove incorrect results. Writing a structured proof does not require much, you can do it simply by using the pf2 package for LaTeX. Therefore, I believe structured proofs à la Leslie Lamport are a necessary tool in the toolbox of the 21st-century mathematician.