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".

Table of contents 152 3
- Conjecture reduction to a halting problem Automated theorem proving by halting problem reduction 71 2
  - Turing machine that halts if and only if the Goldbach conjecture is false (27-state) Conjecture reduction to a halting problem
  - Turing machine that halts if and only if Collatz conjecture is false Conjecture reduction to a halting problem 39

Automated theorem proving by halting problem reduction

 Ancestors (11)