I have recently been reminded of Lamport’s How to Write a 21st Century Proof in more than one way.
Teaching
Last semester I taught two classes. One is a “Intro to Proofs” class, and another is (supposed to be) an advanced undergraduate real analysis course. Upon reflection both of the classes could have benefitted from some inclusion of more structured proofs.
For the “Intro to Proofs” class, this is the belated recognition that “how mathematicians write and read proofs” is not always the same as “how mathematicians think about proofs”. There’s much that can be (and has been) written about this, but the short of the matter is that despite of our pretenses, mathematicians typically don’t write proofs completely rigorously. And we read proofs we don’t often check every detail, but choosing instead to absorb the “big picture”. As such, mathematical proofs that we see presented in graduate level textbooks and in journal articles are frequently really merely “sketches”: there are gaps to be filled by the reader.
What is often neglected in teaching students to read and write proofs is that these proofs or their sketches are backed up, usually, by a concrete and rigorous understanding of the subject. And that the distillation from a complete proof to what is presented on a piece of paper as the sketch is a bit of an art. In some respects a flipped classroom, especially in IBL style, is perfect for this. The students start by presenting proofs in great details, and as they collectively grow more and more may be omitted.
However, what I found disconcerting is that in a regular education, there can be fourth year undergraduate students studying for a degree in mathematics that still have not internalized this difference and are unable to successfully read and write mathematics.
This is where the involvement of more structured proof writing can become useful. Similar to how study of literature involves diagramming sentences, here we diagram proofs. A proof can be written in various levels of details. In a structured presentation these levels can be made explicit: a proof is decomposed into individual landmark statements which taken together will yield the desired result. Each statement will need justification, and the proofs also can recursively be sketched. The final writing of the proof is to prune this tree of ideas by removing the “trivial” justifications and keeping the important ones.
Instructors can demonstrate this in action by preparing detailed proofs of classical theorems in this format. I’ve found that rewriting theorems in this format forces me to re-examine assumptions and conclusions, and overall be more succinct when trying to come-up with a high level sketch. Furthermore, if lecture notes are presented in this format students will also benefit from being able to study the proofs by first obtaining a bird’s eye view of the process and then diving in various levels of detail to the nitty-gritty of the arguments.
I will try to implement this in a future undergraduate math major class and see what happens.
Research
Mathematics papers are getting longer. Especially in my field of hyperbolic PDEs. It is getting harder and harder, when reading a paper, to keep in one’s head a coherent picture of the overall argument. This is a problem that I think can be beautifully solved with more structured approach to presenting arguments.
I am not advocating re-writing proofs as pedantic as Lamport advocates. I am not even advocating the strict presentation. What I do like about the idea of structured proofs is the two-dimensionality of the presentation. In this I am also a bit influenced by Terry Tao’s “circuit-diagram” approach to diagramming proofs that he used in, among other things, his Nonlinear Dispersive Equations book and his recent Averaged Navier Stokes paper.
What I have in mind is the presentation of proofs as nested sketches, but each level written more-or-less in natural language as is currently. Each step of the proof is justified by its own “proof”. The proof can be read at different levels of details, and readers can choose to zoom in and study a portion of the proof when interested. Assumptions and conclusions of individual steps should be made clear; the tree structure of the presentation can help prevent circular arguments. (Some aspects of this is already present in modern mathematical papers: important intermediate arguments are often extracted in the form of lemmata and propositions. This proposal just makes everything more organized.)
This also can improve the refereeing experience. A paper can be rejected if an individual step can be shown to be false. Additional clarifications can be inserted if the referee feels that the paper does not go deep enough in the chain of justifications.
Technological support
This presentation of ideas does not require non-traditional media. But this presentation of ideas can be improved by non-traditional media. I’ve just run into a Web App that does some approximation of what I envisioned: Gingko. It is free to use if your usage isn’t heavy.
What I would love would be for cards to also support
- Cross referencing; currently it supports hashtags, but not referencing with a definite target card.
- Duplicating cards; currently it supports moving, but not duplicating.
- Multiple ancestry: it would be great if the same card can appear as the child of two different cards. But this can also be emulated with cross referencing support or duplication support.
Bubbles Bad; Ripples Good 