tl;dr: In this post I point to two ideas: How to write proofs by Leslie Lamport and how to write reasearch papers by Simon Peyton Jones.

Last week, we had the Heidelberg Laureate Forum here in … well, Heidelberg. I did not participate but I like to read about the event and in particular its invited laureates, as for example on their blog.

One talk that I liked particularly was the one by Leslie Lamport. (Btw.: Some people like to call him “The Turing award winner and father of LaTeX”, but given his publications list that’s both too unspecific and too narrow.) Anyway, I liked his talk about “How to write a 21st century proof”. There is also a paper about the same idea.

I liked the idea of clearly structured proofs. He demonstrates this idea with a proof of a corollary of the mean value theorem in calculus. He does this by taking a conventionally written prose proof from a text book and adding structure and names to it. Pretty much as one would do when trying to teach a computer (proof assistant) the proof. Eventually (in the paper) he even goes all the way to define the proof in his own specification language (TLA+) which can be used as a proof checking language. So he goes from conventional (mostly prose) proof to structured and better readable proof on to not-readable-for-humans-but-for-computers proof. And the middle step is the one I liked very much.

The particular proof that Leslie Lamport has picked for his talk and paper has a linear structure. Therefore, it is easy to enumerate the steps of the proof as a list. However, some proofs don’t have this linear structure but still lend themselves to a depiction by other directed acyclic graphs (See for example this rewrite of Szemeredis theorem by Terence Tao, page 8). But the general idea of dividing a proof into smaller (how small) steps and specifying all the assumptions and conclusions of each step, linking them to a directed acyclic graph is a very natural way to do this.

The difficult questions are of course how small should the steps be and how much detailed should be added to each step. But Lamport also answers this question: Make it hierarchical and use modern tools (in this case hypertext). This way one can expand or collapse each part of the proof and hide details from the eyes of sophisticated readers. If one cannot use hypertext, the only solution is to make an assumption and imagine a particular reader. This reader can be a little curious kid (as in the paper’s proof from the freshman calculus book) or a fields medalist reading your latest research article.

For me personally, it sounds like an interesting idea to extend the idea of less prose and more structure to scientific articles. But of course, this has already been done by Lamport’s fellow Microsoft employee (and Haskell inventor (again the question: is this fair to him or the other Haskell inventors)) Simon Peyton Jones in his article and talk How to write a great research paper.

One thing that I don’t like about papers can be captured by the following quote from Jones’ talk:

I also agree with Jones in that I don’t like it when authors put the related work section in the beginning and therefore build a hill or wall over which the reader has to climb to get to the actual results. I think a good approach to this problem would be the same way that Lamport proposed in his talk: Add structure and hide the details in the lower levels of the hierarchy.

If I find the time I will try to exemplify this at few papers from my field.