Halting problem vs. automated theorem proving?

Question

In the Theory of Computation tutorial offered by Complexity Tree (I just began the 2nd video), it talks about how the Halting problem was developed to show that mathematics could not be automated. Lately, I've heard quite a bit about automated/automatic theorem proving--some people are even positing that some day mathematicians will be replaced by machines. My question is: Do we need to find a flaw in the reasoning of the Halting problem to prove that mathematics can be automated? (Or is the Halting problem, in the age of Machine Learning, reduced to a nice historical account of the past...)

Answer 1

The notion of automating mathematics is a vague one, and that's accounting for the discrepancy here.

One interpretation would be: to automate mathematics would be to produce a machine $M$ which could tell whether or not a given sentence is true (or, more weakly, provable from some agreed-upon set of axioms like $\mathsf{ZFC}$). Even the weaker version is ruled out by the incomputability of the halting problem.

Another interpretation is: to automate mathematics is to produce a machine $M$ which will find proofs of all provable (again, from that agreed-upon set of axioms) sentences. Note that $M$ is not required to determine whether a sentence is provable in the first place, merely to find a proof if such a proof exists at all. This is possible via brute force search.

Of course that second type of automation is highly infeasible - in general, it will take ridiculously long to find proofs of theorems. But that doesn't impact its in-principle-possibility. This is really the starting point of automated theorem proving: trivially brute-force-proof-search is possible, and trivially it's horrible in general - can we find clever proof search strategies in some cases of interest? (And this is where complexity theory enters the picture.)

Answer 2

You are conflating two possible meanings of the phrase "mathematics can be automated":

1. "any theorem can be proved true or false by an algorithm"
2. "the practical activity of proving theorems, as presently performed by humans, can instead be performed by computers in an economically-viable fashion"

Due to the halting problem, it is impossible for any algorithm to be able to prove or disprove all theorems. But this applies just as well to humans as to computers!

There does not need to be a flaw in the proof of the halting problem's undecidability for (theoretically) the job of human mathematicians to become obsolete. A machine does not have to be able to solve undecidable problems to eliminate the job function of human mathematicians—it just has to be able to prove theorems of interest more efficiently than humans can. This is a not a question of computability or asymptotic computational complexity but of economics.

There is no reason to think that human brains are uniquely superior in proving mathematical theorems. Moreover, due to Moravec's paradox, we should expect that computers might be better at proving theorems than humans. A human brain is a sack of meat whose evolutionary history includes virtually no fitness rewards for the phenotype of "can prove difficult theorems." So we would expect that we might see a computer that is superintelligent in the area of proving theorems sooner than we would expect to see a computer that is superintelligent in the area of, say, hunting megafauna.

Answer 3

I think this question should give you the answer.

https://cstheory.stackexchange.com/questions/2800/if-p-np-could-we-obtain-proofs-of-goldbachs-conjecture-etc

In short, if P=NP then any conjecture with a reasonable length proof can be proved by a computer.