Automated theorem proving by halting problem reduction

If you can reduce a mathematical problem to the Halting problem of a specific turing machine, as in the case of a few machines of the Busy beaver scale, then using Turing machine deciders could serve as a method of automated theorem proving.

That feels like it could be an elegant proof method, as you reduce your problem to one of the most well studied representations that exists: a Turing machine.

However it also appears that certain problems cannot be reduced to a halting problem... OMG life sucks (or is awesome?): Section "Turing machine that halts if and only if Collatz conjecture is false".