{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}.


Automated theorem proving by halting problem reduction

ID: automated-theorem-proving-by-halting-problem-reduction