The first thing that struck me from Lamport’s examples here of structured proofs is how similar they are to a common way K-12 math initially teaches students to write proofs, the “two-column proof” structure. A two-column proof has a sequence of numbered statements in the left column, each of which must be justified by reasons noted in the right column. The reasons can be either appeals to a previous numbered statement, or to a named theorem/lemma already introduced in the textbook. Instead of using the second column, Lamport instead writes “PROOF: …” and gives the justification below each numbered statement, but it otherwise seems pretty similar.

The other main difference, of course, is that he thinks it would be a good idea to use this in professional mathematics work rather than only in pedagogy. This brief dismissal is probably representative of the opposite view. It’s a bit surprising that Lamport therefore didn’t discuss two-column proofs (perhaps he hasn’t run across them?). He makes it sound like mathematicians haven’t thought of writing proofs this way, when I think the current situation is rather than they’ve thought of it and even teach it, but consider it only useful as a pedagogical tool, and too cumbersome for real work. That’s the part he really needs to convince them is wrong.

Every time structured hand-written proofs come up, I think of my 9th grade geometry class where we learned how to do two-column proofs. At least for me, the presentation was far too informal for it to really “click” with me what the core rules of logic were. Recently I’ve been learning how to use Isabelle/Isar, which is a structured proof language built on top of the Isabelle proof assistant framework. It’s quite refreshing compared to the usual unstructured proofs in Isabelle or Coq. In my personal education, learning how to reason with natural deduction-style systems was hugely helpful for actually learning at a deep level how proofs and logic mix together and work. I think there are some serious improvements that could be done to early math education using more formal systems.

I’m not a professional mathematician (yet) and can’t comment on any issues there. I will point out the growing Archive of Formal Proofs, http://afp.sourceforge.net/. It seems promising!

The first thing that struck me from Lamport’s examples here of structured proofs is how similar they are to a common way K-12 math initially teaches students to write proofs, the “two-column proof” structure. A two-column proof has a sequence of numbered statements in the left column, each of which must be justified by reasons noted in the right column. The reasons can be either appeals to a previous numbered statement, or to a named theorem/lemma already introduced in the textbook. Instead of using the second column, Lamport instead writes “PROOF: …” and gives the justification below each numbered statement, but it otherwise seems pretty similar.

The other main difference, of course, is that he thinks it would be a good idea to use this in professional mathematics work rather than only in pedagogy. This brief dismissal is probably representative of the opposite view. It’s a bit surprising that Lamport therefore didn’t discuss two-column proofs (perhaps he hasn’t run across them?). He makes it sound like mathematicians haven’t thought of writing proofs this way, when I think the current situation is rather than they’ve thought of it and even teach it, but consider it only useful as a pedagogical tool, and too cumbersome for real work. That’s the part he really needs to convince them is wrong.

Every time structured hand-written proofs come up, I think of my 9th grade geometry class where we learned how to do two-column proofs. At least for me, the presentation was far too informal for it to really “click” with me what the core rules of logic were. Recently I’ve been learning how to use Isabelle/Isar, which is a structured proof language built on top of the Isabelle proof assistant framework. It’s quite refreshing compared to the usual unstructured proofs in Isabelle or Coq. In my personal education, learning how to reason with natural deduction-style systems was hugely helpful for actually learning at a deep level how proofs and logic mix together and work. I think there are some serious improvements that could be done to early math education using more formal systems.

I’m not a professional mathematician (yet) and can’t comment on any issues there. I will point out the growing Archive of Formal Proofs, http://afp.sourceforge.net/. It seems promising!