[fspeech]

The flimsiness of one's understanding tends to manifest as false "lemmas", which can't really be proved because one forgot certain conditions that are typically implicit with human understanding but must be made explicit formally. However if a proof can be completed then it's solid by definition. I would contend when a proof becomes hard to understand instead of documenting tactics one should break up the proof into more lemmas or create more subgoals; preferrably all tactics are "auto". It's nice that the tool you referred to is general and can be used to document any prospect of proof but being based on a markup language it is mostly static. When Gonthier mechanized Feit-Thompson Odd Order Theorem, he had very large graphs showing the relationship of the lemmas. Unfortunately those were also static as I remember and only really comprehensible to the experts. It would be nice to have interactive versions that can aid an average reader on comprehending and exploring the overall relationships. Such a tool is also sorely missing for understanding large code bases. The two are really two sides of the same coin through Curry-Howard. The good thing is a tool that lets users efficiently navigate structures can be done without extra effort of the proof writer (of course documenting intention is always important).