The Curry-Howard isomorphism doesn't explain away mathematics. There are next to zero large and important theories of mathematics which have been formalized in

The Curry-Howard isomorphism doesn't explain away mathematics. There are next to zero large and important theories of mathematics which have been formalized in a computer language. It's partly due to the difficulty of proof automation---the solvers are very young---but mostly because proofs are just the pickaxes for mathematics. Right now human-driven proofs are far more powerful tools. Programming benefits greatly from a tiny section of mathematics and the more deeply the connection between the fields grows the more we'll see strong justification for universal patterns in programming and strong realization of abstract mathematics. It's also a bit of a strawman to pick just number theory as the only field of mathematics to examine for practicality. Our world as we know it today would not exist without diffeq and your own example of machine learning really is just applications of optimization, statistics, probability, and abstract geometry. "We need them both" is an unrefined statement. They are apples and oranges, though a mathematical programmer might be uniquely powerful as might a programming mathematician (Djikstra?).