I think you are missing the point. Solving a problem using mathematics is EQUIVALENT to solving a problem using computation (which is a silly truism, because y

I think you are missing the point. Solving a problem using mathematics is EQUIVALENT to solving a problem using computation (which is a silly truism, because your mind is a computer). They are two different mind-instruments, two frameworks for thinking and thinking about thinking. They are functionally identical What you can do with one - you can do with the other. Because Mathematics can only prove things up to an isomorphism. And Curry-Howard is an isomorphism. Whether any particular solution can be automated is not my point at all. My point is that when a human solves an abstract problem - they express the solution in language. Some humans speak Mathematics. Some humans speak Python. The divide between Mathematics and Computer science is cultural, not grounded in utility. Hence why - I would love to see some unification.