3 ms·
> even though he was talking about the applied side, it goes perfectly for the more abstract areas too. This is where Bret Victor and I disagree: interactive d
by j2kun 12y ago
> even though he was talking about the applied side, it goes perfectly for the more abstract areas too.
This is where Bret Victor and I disagree: interactive documents for visualizing circuit diagrams do not generalize perfectly to all of mathematics. If you want to develop a generic tool that allows any mathematician to build interactive documents for tinkering with concepts, you need to see how deep the mathematical rabbit hole goes. Victor's tools are a proof of concept for very limited systems.
- pas 12y agoWhen I was studying mathematics the tool I wanted most was a simple proof assistant that could help me dive deeper into steps. Because to effectively understand a concept (usually through applications of it either in full blown proofs, or in smaller calculations - that are just ad-hoc proofs) you need the right level of verbosity. Oversaturation with low-level set theory steps from Burbaki won't make anyone understand systems of differential equations, but when you are unsure of a step, you need a bit more detail. And in my experience the optimal trajectory through a proof is almost always different for everyone. So it'd be good if proofs were "discoverable", expand and collapse steps. And we don't even have to go crazy with "reverse mathematics"-like axiom chasing. But the current practice of throwing random symbols on pages in LaTeX is rather suboptimal in my opinion.
- j2kun 12y agoThis is not an interactive document in the sense Bret Victor proposes.