= Automated theorem proving by halting problem reduction
{tag=Automated theorem proving}
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?): <Turing machine that halts if and only if Collatz conjecture is false>{full}.