25

In 1995, Leslie Lamport published an essay in the American Mathematical Monthly titled "How to write a proof". In the essay, Lamport introduced the concept of a structured proof, in which the traditional high-level proof is augmented by a sequence of lower levels. Each level of proof expands each step of the higher level into substeps. The amount of detail at the lowest level is rather extreme -- Lamport's proof of the irrationality of the square root of 2 runs to 1.5 pages.

The essay has over 250 citations according to Google Scholar, but I have never seen a proof published in this format. In a PDF or on paper, the extreme detail could be overwhelming; but I think modern web publishing platforms could accommodate it very well (with hierarchical collapsible subsections for each part of the proof).

In any case, are there examples of proofs published in the format suggested by Lamport?

Improve this question
11
  • 1
    I like the collapsible idea! Have you asked about this over at matheducators.stackexchange.com? It seems like this would be especially useful for students.
    – aparente001
    Commented Aug 31, 2015 at 2:59
  • 2
    Somewhere on the internet is a whole book full of structured proofs (à la Lamport, and maybe even with his coauthorship). As far as I remember, its goal is to prove the correctness of some software, but a good part of it is basic mathematics; can anyone find it?
    – darij grinberg
    Commented Sep 12, 2015 at 14:25
  • 2
    Ah, found that book! Thomas L. Rodeheffer, The Naiad Clock Protocol: Specification, Model Checking, and Correctness Proof, research.microsoft.com/apps/pubs/?id=183826 .
    – darij grinberg
    Commented Sep 12, 2015 at 14:41
  • 2
    Apparently research.microsoft.com/en-us/um/people/lamport/tla/… is a good introduction into structured proofs, with lots of examples.
    – darij grinberg
    Commented Sep 12, 2015 at 14:44
  • 1
    Everything so far in the comments and the one current answer indicates that you can find plenty of structured proofs, and every last one of them has Lamport's hand in it. So, apparently, nobody but Lamport and his coworkers at MS use it.
    – zibadawa timmy
    Commented Sep 12, 2015 at 22:41

1 Answer 1

Reset to default
5

While most people use more traditional proof styles, the more exhaustive structured proof style that Lamport proposes seems to be adopted, at least in spirit, by machine-assisted proving systems like Coq and Lamport's own TLA+. By bringing a very non-intuitive player into the loop (the machine), these systems force the mathematician to be much more explicit about every step and assumption, and encourage hierarchical structure by their use of programming-language style syntax.

These proving systems are typically quite expensive to use, and you generally wouldn't want to put their lengthy proofs into the middle of a paper---attaching as supplementary information is more the way to go. They are, however, proving to be quite valuable in critical applications where dealing with every possible edge case is important, such as in the design of microprocessors or cryptographic protocols.

Improve this answer
4
  • 1
    Modern Coq proofs written in ssreflect (e.g., github.com/hivert/Coq-Combi ) are actually not that long! The problems, as far as I can discern them from (unfortunately) somewhat afar are (1) that the Coq format does not easily support human readability (it is very hard to follow a Coq proof on pen and paper), (2) that lack of function extensionality and (lack of) good support for setoids make a lot of mathematical constructions forbiddingly hard to deal with (forget about encoding a tuple of elements of $A$ as a map $\left\{1,2,\ldots,n\right\} \to A$; the ...
    – darij grinberg
    Commented Sep 12, 2015 at 14:47
  • 1
    ... ssreflect people, conversely, seem to define maps between finite sets as tuples with certain properties, just because tuples know how to be equal!), and (3) that the infrastructure is still very much in flux and proofs might break with the next update of Coq or ssreflect. But this is absolutely a thing that will work one day.
    – darij grinberg
    Commented Sep 12, 2015 at 14:48
  • And there I was like "why the hell doesn't my LaTeX work?". This question really should be on mathoverflow.
    – darij grinberg
    Commented Sep 12, 2015 at 14:58
  • Thanks! This is interesting, though I don't believe these are examples of exactly what I asked for.
    – David Ketcheson
    Commented Sep 13, 2015 at 7:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .