Automated proof-checking machine

Question

In the future, theoretically, is it possible to make an automated proof-checking machine?

It means, given mathematical axioms and definitions, the computer can decide that a proof is correct or not, even though the proof is very complex.

Some people may say that it is impossible the construct such machine because there is a proof that algorithm machine cannot decide it is correct or not , even though the proof is correct proof for a problem.

This proof-checking machine is different from proof-solving machine. The proof-checking machine don't provide proofs. It just decide given proof is correct or not.

Say again: There is a proof. Human can decide the proof is correct proof. But computer cannot decide the proof is correct or not. Is this situation possible?

Answer 1

There is an algorithm which, given a recursive description of the axioms of a first-order theory $T$, and a purported proof from $T$ of a sentence $\varphi$, can decide whether that proof is correct. Certainly one can write a computer program that will execute that algorithm. The task is not even difficult.

The fact that there is an algorithm that works is contained in the usual proofs of the Soundness and Completeness theorems.

The question becomes more complicated when we are dealing with human proofs that are "correct" but not fully formal. Can a computer program fill in the "gaps"? In principle, if there is a proof, one can write a program that will find one. So the question becomes now not a question of logic, but of finding practical implementations. In some areas, unfortunately rather restricted, we are quite close to having that.

Answer 2

The issue here is the language in which you write your proof. Depending on its strength it might be

• impossible, e.g. when the language contains halting problem oracle,
• inconvenient, e.g. when the input is in natural language (which is too ambiguous),
• it might have been already done, e.g. see Coq.

I hope it answers your question ;-)