I think people already do write things in a hierarchical way. They have one main theorem which is supported by multiple propositions and lemmas and corollaries.

I think people already do write things in a hierarchical way. They have one main theorem which is supported by multiple propositions and lemmas and corollaries. At least, this is how all good papers I read are organized. I think Lamport's vision is that the hierarchy extends down to the very last detail. This is what I'm skeptical of, because no mathematician has time to do this. To paraphrase Newton, you need to stand on the shoulders of giants to make progress.