> They seem to think that if they can make a tool that allows them to read calculus textbooks or machine learning textbooks more easily, this tool will obviously be useful for all mathematicians everywhere. I disagree.
I agree with you times infinity.
I get frustrated when programmers are used to looking at source code that has very precise meaning and are expecting to be able to read mathematics as if it were source code too. Or worse, when people think that the hardest part of understanding mathematics is the notation. Or that a capital sigma means a sum in all contexts, or that a lowercase sigma could not possibly mean anything other than a standard deviation or a lowercase pi could not mean anything other than the first positive root of the sine function.
Mathematics is written by humans for humans. Trying to automate mathematical writing or reading is about as feasible as trying to automate literary analysis of 19th century romanticism[1]. Or in Weierstrass's words to Kovalevskaya,
[...] it is true that a mathematician who is not somewhat of a
poet, will never be a perfect mathematician.
[1] When reading Riemann, I particularly feel like I might as well be reading E. T. A. Hoffman sometimes. Some of the moves he makes I cannot describe as anything but poetical. For example, how he describes the contours of integration in a couple of reformulations of the zeta function.
Sure. But since I can't directly probe your mind, I can either read through thousands of pages of manuscript to refine my internal mental model of the particular theory/problem set/subfield, or hope for an interactive system that allows me to do just that, where I can tinker with concepts and connections between them.
Bret Victor showed it best, and even though he was talking about the applied side, it goes perfectly for the more abstract areas too.
> 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.
When 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.
I agree with you times infinity.
I get frustrated when programmers are used to looking at source code that has very precise meaning and are expecting to be able to read mathematics as if it were source code too. Or worse, when people think that the hardest part of understanding mathematics is the notation. Or that a capital sigma means a sum in all contexts, or that a lowercase sigma could not possibly mean anything other than a standard deviation or a lowercase pi could not mean anything other than the first positive root of the sine function.
Mathematics is written by humans for humans. Trying to automate mathematical writing or reading is about as feasible as trying to automate literary analysis of 19th century romanticism[1]. Or in Weierstrass's words to Kovalevskaya,
https://en.wikiquote.org/wiki/Karl_Weierstrass[1] When reading Riemann, I particularly feel like I might as well be reading E. T. A. Hoffman sometimes. Some of the moves he makes I cannot describe as anything but poetical. For example, how he describes the contours of integration in a couple of reformulations of the zeta function.