Halting problem vs. automated theorem proving? 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...)
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.)