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.
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).
An automated factory cannot build any possible car. But we no longer need to have people hand assembling the components.
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) 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).