Indeed, what I'd like is formal mathematics proving language that could be viewed as an outline in that natural language math proofs are structured as outlines. The reader would be able to choose what to view - definitions, theorems, lemmas, examples, key-steps, all steps etc.

Ideally, a view would let a reader expand into not just the proof at hand but the various theories in the repository.

A reader could even tell their viewing preferences and it might strip down the UI for those purposes.