On: Don’t Kill Math
Link: Don’t kill math
A case for analytic method of learning vs a more visual one. There are obvious advantages to learning math the simulation/visualization way and the symbolic way. There are two points that come to my mind after reading this:
Bret Victor’s “new“ approach isn’t the first one that tries to deal with mathematics in a post-computing era. While many mathematicians utilise modern computers in their daily research, the original method for learning mathematics perhaps hasn’t changed in decades (this is, however, not from first-hand experience, but by reading articles from other mathematicians). Data visualization, Python or R have become ubiquitous in statistics and machine learning. Since I am not a physicist I can’t be one hundred per cent sure, but even Physics now heavily depends on computer simulations and data analysis.
But “pure“ mathematics seems to have eluded computer utilization up until recently. When it comes to higher level, abstract math, I can think of only two ways to move away from the symbolic approach: theorem provers and LLMs. The latter is an immature and extremely infant technology, hence we must wait to see it’s converging destination. However, the former is an interesting topic. To be precise:
Why not use theorem provers to even teach mathematics, and build intuition ?
What I am suggesting is, in my opinion, the modernization of mathematics. The traditional methods of learning mathematics can be replaced by modern strongly and extremely expressively typed programming languages, which have multiple benefits.
Instead of relying on arbitrary problem-solving and back-of-the-chapter questions to build strong intuition, we are literally forced to build intuition by explicitly writing various concepts in a programming language.
Proofs are immediately checked by the system, providing faster feedbacks (as opposed to having another person check ones proofs).
Any arbitrary definition can be shared, without past material or context (due to each mathematician having their own compiler and libraries). This could give math the same reach and democratizing effect as computer science.
Perhaps this is already being followed, I am not sure. But these advantages are there, and force one to remove any and all ambiguities about mathematics (especially pure and higher-level abstract) by writing concrete and typed definitions.
That being said, programming languages (even ones like Idris, Agda, Lean or Coq) have a long way to go before being expressive enough to encode some mathematical theories. Thinking in terms of types may also somehow constrain ones thinking in a particular direction, and bias certain results while obscuring others. This would be made clear if there is a mass adoption of learning math purely through a typed programming language.