Comment by joe_the_user
3 days ago
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.
Yes, I had similar thoughts last week: https://news.ycombinator.com/item?id=49995658
> proper IDE for math
Love this concept, and the potential for a far more integrated interface with various features that smartly supports the author, like a structural/projectional editor with built-in understanding of mathematics.