2

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?

vonbrand
  • 27,812
martian03
  • 75

2 Answers2

5

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.

André Nicolas
  • 507,029
  • Thank you Andre. But I am still confusing. You said, "we have a first-order theory T, with a recursive set of axioms".... If the proof is in ZFC system. (ZFC axiom system), do we still need the assumptiom of first-order theory? – martian03 Mar 08 '13 at 18:01
  • 1
    ZFC is a first-order theory, and it is in principle (and practice) quite easy to check whether a fully formalized proof in ZFC is correct. However, for practical implementation, it is useful to work with less rich theories. – André Nicolas Mar 08 '13 at 18:11
  • Thanks again Andre. If the machine exist, how efficient is the machine? Is it possible that the machine run in polynomial time? – martian03 Mar 08 '13 at 18:27
  • 2
    Checking an existing formal proof is very fast. Depends on implementation details, but quadratic time is no problem. I expect one can do better than quadratic. – André Nicolas Mar 08 '13 at 19:06
  • What about "natural proof"? Even though the proof is not "natural proof" but it is in ZFC, does the machine stiLl work? – martian03 Mar 08 '13 at 23:09
  • @HoCheolSHIN: I do not understand the question. The proof verification process certainly works for ZFC, since this theory is recursively axiomatized. – André Nicolas Mar 08 '13 at 23:16
  • Sorry. I need to study more about natural proof. Andre, I have final question about this topic. The specific-problem-proof-checking machine can exist? For example, there is a Riemann hypothesis proof-checking machine. When the proof is about Reimann hypothesis, and proving or disproving (or concluding undecidable) process is logically correct, the machine say "yes". If the proof is not correct, machine say "no". If it is not about Reimann hypothesis (even though it is correct), the machine say "no". For example, for the statement "4 is even number", the machine say "no". Is this possible? – martian03 Mar 08 '13 at 23:53
  • 1
    Yout original question asked about formal proof checking, Now you are asking about undecidability, which is entirely diifferent. Also, it is easy to cehck whether a claimed proof proves a certain result. "About" is imprecise: one never knows whether something like the theory of elliptic curves will ultimately lead to say, Fermat Last Theorem. If you have other concrete questions, do post again, then you may get answers from several people. – André Nicolas Mar 09 '13 at 00:30
  • Thanks. "proof about' means, a proof that insist that the property of the conjecture is true or not or undecidable. For example, a proof about Fermat Last Theorem means a proof that insist the equation x^n + y^n = z^n is possible or impossible. Anyway, I will post a new post as you recommended. – martian03 Mar 09 '13 at 08:56
  • Thanks for explaining what was meant by proof about. I should have been able to understand from context. The answer I gave dealt with fully formal systems. So we can certainly check a proof of undecidability of a proposition of $T$, if that undecidability proof is a ZFC proof. But the Incompleteness Theorem shows they cannot all be. – André Nicolas Mar 09 '13 at 13:56
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 ;-)

dtldarek
  • 37,381