[thejaredhooper]

This could have been more precise. The example at the start was great, but there's no example of the lecturer's technique outside of the link to the actual lecture

[NSMeta]

There's a link to his paper:

http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

[qznc]

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

[1] Not really surprising. Lamport invented LaTeX.

[orbitur]

Right. It would have been nice to have a short yet more in-depth example in the article.