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