Automatic proof verification by a Turing machine

Question

Is it possible to automatically verify a mathematical proof? Or is it proven that this cannot be done by a Turing machine?

Thank you very much

Kevin

Answer 1

It is completely possible if you work with a recursive theory, such as ZFC. Everything required to check a proof is trivially done by a Turing machine, you just have to recognize an axiom when you see one, hence the fact that the theory must be recursive.

On the other hand, finding a proof is impossible.

Answer 2

To build off the other answer, the question of finding a proof is Hilbert's Entscheidungsproblem, in which case the answer is that no such algorithm exists. On one level, Godel's Theorems say that some true statements don't have proofs. But even if we know a theorem either has a proof or has a disproof, it's still impossible.

The crux of the issue here is that you don't know how long a proof of a theorem is. If the shortest proof or disproof of $T$ is denoted $\ell(T)$, then the fact that $\ell(T)$ can be incredibly long, and in fact it can be a noncomputable function of $T$.