9 ms·

There's a link to his paper: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p.

• orbitur 12y ago
  Right. It would have been nice to have a short yet more in-depth example in the article.
• qznc 12y ago
  After reading that, I think structured proofs should be written with an outliner [0] interface, where you can actually expand and collapse the hierarchy. Lamport also knows this. He repeatedly mentions it as "hypertext". However, he seems to be locked into LaTeX [1] and pdf generation. [0] https://en.wikipedia.org/wiki/Outliner https://en.wikipedia.org/wiki/Outliner [1] Not really surprising. Lamport invented LaTeX.