I want an environment for proofs and/or mathematical explanations, which treats them as a tree or a graph rather than text. More specifically, I want to be able to write proofs like:
* Suppose A
* From A it follows that B
* C can be proved by induction
* Because B implies not C, it follows that A is false

And if you click on "C can be proved by induction", you get a more detailed explanation of how that happens:
* What property exactly we're proving by induction
* How base case is proved
* How inductive step is proved

And there somewhere if you see a logical step and you're not sure what theorems we invoke to prove it, you click on it and see "by lemma 2.2 (ii)"

There's an article by Leslie Lamport (link to article: https://www.microsoft.com/en-us/research/uploads/prod/2016/12/How-to-Write-a-21st-Century-Proof.pdf; link to hacker news discussion: https://news.ycombinator.com/item?id=17430577)
in which he advocates writing a more structured way of writing proofs, which goes like this:

1. A
2. A implies B
3. not C
4. B implies C, hence not B, hence not A

Proof of 1:
blah blaah

...

Proof of 4:
safdlkjaslfdjafds

What other similar things are there?

http://workflowy.com/ - a TODO program where you simply have nested lists, and you can easily expand or collapse subtrees

https://waitbutwhy.com has these circles of different colors in text. Green circles are interesting footnotes, grey ones are boring footnotes. This doesn't allow creating trees of arbitrary depth but the usability of these things is very good in my opinion and perhaps we don't need that much depth.

It seems http://arbital.com/ has a thing like waitbutwhy, except it allows arbitrary depth.