On 2016-10-11 10:56, Hubert Chathi wrote:
> I suspect that it will be a long time before hierarchical proofs gain
> much popularity though, given that Lamport has been talking about them
> since at least the 90's, and I haven't seen one "in the wild" yet.

Depends how much you're willing to stretch the definition.  Many machine-checked proofs are written in a pretty hierarchical style, and some of the associated tools support folding and expanding subproofs (see the middle gif in https://github.com/cpitclaudel/company-coq/#outlines-code-folding-and-jumping-to-definition).