There's a relationship between the incompleteness theorems and the halting problem in that no turing machine can decide whether an arbitrary statement in a logi

There's a relationship between the incompleteness theorems and the halting problem in that no turing machine can decide whether an arbitrary statement in a logical system where the incompleteness theorems apply is derivable or not. Equivalently, there's no turing machine with input 'statement in the logical system' and outputs a proof or a "unprovable". However, once you already have a proof, checking is much easier (at the formal level). Modern mathematical proofs, however, are not generally written in a fashion in any way similar to how the formal system operates, so applying this in practice is non-trivial.