4 ms·

He's not saying mathematics doesn't have rigorous foundations. Betrand Russell's Principia Mathematica is computation. But math textbooks/papers are not like t

He's not saying mathematics doesn't have rigorous foundations. Betrand Russell's Principia Mathematica is computation. But math textbooks/papers are not like this. They share insights, opinions, and metaphors, and frequently explain things in non-rigorous terms, although these are not substitutes for proofs even though proofs for something given a non-rigorous explanation may not appear. In less heavily proof-read contexts, such as in discussions or a class room, it's not uncommon for mathematicians to be pretty free-wheeling with their notation, and leave it up to context and intuition to figure out what an individual symbol means at a given time. And it wouldn't be a faux pas, or sign of a lesser mathematician or anything like that. These things can be valuable and in some sense are a part of mathematics. Although the end results of mathematics can be distilled into formal computations, it's far too reductive to say that's all mathematics is.

ukj 7y ago
The exact same thing can be said about any human dynamic where the objective is to teach. The end-goal is to make the material accessible to the learner by connecting it some pre-existing human intuition or experience, thus providing the learner with a vocabulary to express their thoughts. The important question is how are the vocabularies (both formal and informal) produced by Mathematics different from the vocabularies produced by Computer Science when both fields are working on the same real-world problems? And if the two vocabularies are of equal utility - do we really need two different tools for the same job?
- jcranberry 7y ago
  Computer science and mathematics do not work on only the same problems or produce the same results, except for the parts which overlap. Unless you're attributing results by automated theorem provers as results in computer science? The point of mathematics being expressed in these ways isn't just teaching. Mathematics may be abstract, but it is still fundamentally abstracting patterns which arise from the human experience (for the most part). Tying mathematics back to human experience is an important aspect of the discipline. But another important reason is to engender further research and advancements. What you're saying is exactly asking whether programs can replace programmers, since you can design a program which generates programs. Mathematics and computer science are human disciplines with results whose purpose is to find results which are of interest to humans. At this point we are able to sometimes verify theorems and occasionally prove a theorem automatically. But ATPs are unable to write comprehensible proofs, tell what corollaries may be of interest, or to autonomously build off of theorems in directions which would interest us. At this point they are not necessarily able to prove theorems in reasonable time frames. Furthermore the results produced by vocabulary are not just theorems. High quality proofs are just as valuable. They tell us why things are true in ways which are significant or profound. Although the 'why' is not necessarily useful, it is still of interest to mathematics. Perhaps ATPs will be able to accomplish all this eventually. But currently they don't provide the same utility as mathematics.
  - ukj 7y ago
    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.

ukj 7y ago

The exact same thing can be said about any human dynamic where the objective is to teach. The end-goal is to make the material accessible to the learner by connecting it some pre-existing human intuition or experience, thus providing the learner with a vocabulary to express their thoughts. The important question is how are the vocabularies (both formal and informal) produced by Mathematics different from the vocabularies produced by Computer Science when both fields are working on the same real-world problems? And if the two vocabularies are of equal utility - do we really need two different tools for the same job?

jcranberry 7y ago
Computer science and mathematics do not work on only the same problems or produce the same results, except for the parts which overlap. Unless you're attributing results by automated theorem provers as results in computer science? The point of mathematics being expressed in these ways isn't just teaching. Mathematics may be abstract, but it is still fundamentally abstracting patterns which arise from the human experience (for the most part). Tying mathematics back to human experience is an important aspect of the discipline. But another important reason is to engender further research and advancements. What you're saying is exactly asking whether programs can replace programmers, since you can design a program which generates programs. Mathematics and computer science are human disciplines with results whose purpose is to find results which are of interest to humans. At this point we are able to sometimes verify theorems and occasionally prove a theorem automatically. But ATPs are unable to write comprehensible proofs, tell what corollaries may be of interest, or to autonomously build off of theorems in directions which would interest us. At this point they are not necessarily able to prove theorems in reasonable time frames. Furthermore the results produced by vocabulary are not just theorems. High quality proofs are just as valuable. They tell us why things are true in ways which are significant or profound. Although the 'why' is not necessarily useful, it is still of interest to mathematics. Perhaps ATPs will be able to accomplish all this eventually. But currently they don't provide the same utility as mathematics.
- ukj 7y ago
  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.