3 ms·

The Entscheidungsproblem says that proving theorems is at least as hard as the halting problem. This seems irrelevant to the issue of whether human input is ess

by Khaki 12y ago

The Entscheidungsproblem says that proving theorems is at least as hard as the halting problem. This seems irrelevant to the issue of whether human input is essential for finding or proving interesting theorems.

JadeNB 12y ago
I agree that I should not have singled out automated mathematics as uniquely vulnerable—human efforts at formalisation are also subject to limitations. I was also conflating Turing's work on the Entscheidungsproblem with Gödel's not-unrelated but meaningfully distinct incompleteness results, which are more relevant to the point that I was trying to make. Nonetheless, I point out that I did not claim that human input was essential either for finding or proving interesting theorems (although proveable results about (non-)computeability seem as close as one could get to such a statement!), but only that math could never be completely automated (or, to use what, as you implicitly point out, is a more appropriate term, even formalised).
- kazagistar 12y ago
  I think the problem is a disagreement on what kind of "automation" is the goal. You seem to want to automate all possible math. Sure, we can't do that. But we certainly can try to automate any math a human can do (eventually). An automated factory cannot build any possible car. But we no longer need to have people hand assembling the components.
  - JadeNB 12y ago
    > I think the problem is a disagreement on what kind of "automation" is the goal. You seem to want to automate all possible math. Sure, we can't do that. But we certainly can try to automate any math a human can do (eventually). This is a very helpful reply; thanks. I don't want to automate all math, since it is impossible to do so; and I think that I have clearly indicated in each of my posts in this thread that I am speaking only to that particular, narrow issue—but I can see how that narrow nit-picking might not be of interest. The reason that I brought it up was because it sounded to me like what pnut (https://news.ycombinator.com/item?id=8169453 https://news.ycombinator.com/item?id=8169453) was suggesting. Now, I do not believe that computers can automate any math that a human can do, except in the narrow sense that I might be able a posteriori to tell a computer to follow exactly the steps that I took. (Some 'intuitive' processes are presumably not subject to automation even in this very weak sense.) This is a much stronger assertion requiring much stronger demonstration, and I am not prepared to (nor, I think, have I claimed to) address it. Perhaps, with that caveat, that's the discussion that I should have started (with perhaps my weaker point as a footnote).

by Khaki 12y ago

JadeNB 12y ago

I agree that I should not have singled out automated mathematics as uniquely vulnerable—human efforts at formalisation are also subject to limitations. I was also conflating Turing's work on the Entscheidungsproblem with Gödel's not-unrelated but meaningfully distinct incompleteness results, which are more relevant to the point that I was trying to make. Nonetheless, I point out that I did not claim that human input was essential either for finding or proving interesting theorems (although proveable results about (non-)computeability seem as close as one could get to such a statement!), but only that math could never be completely automated (or, to use what, as you implicitly point out, is a more appropriate term, even formalised).

kazagistar 12y ago
I think the problem is a disagreement on what kind of "automation" is the goal. You seem to want to automate all possible math. Sure, we can't do that. But we certainly can try to automate any math a human can do (eventually). An automated factory cannot build any possible car. But we no longer need to have people hand assembling the components.
- JadeNB 12y ago
  > I think the problem is a disagreement on what kind of "automation" is the goal. You seem to want to automate all possible math. Sure, we can't do that. But we certainly can try to automate any math a human can do (eventually). This is a very helpful reply; thanks. I don't want to automate all math, since it is impossible to do so; and I think that I have clearly indicated in each of my posts in this thread that I am speaking only to that particular, narrow issue—but I can see how that narrow nit-picking might not be of interest. The reason that I brought it up was because it sounded to me like what pnut (https://news.ycombinator.com/item?id=8169453 https://news.ycombinator.com/item?id=8169453) was suggesting. Now, I do not believe that computers can automate any math that a human can do, except in the narrow sense that I might be able a posteriori to tell a computer to follow exactly the steps that I took. (Some 'intuitive' processes are presumably not subject to automation even in this very weak sense.) This is a much stronger assertion requiring much stronger demonstration, and I am not prepared to (nor, I think, have I claimed to) address it. Perhaps, with that caveat, that's the discussion that I should have started (with perhaps my weaker point as a footnote).