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).
