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.

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