Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.
|
|
|
|
Re: Yes, proof checkers exist!
Posted:
Dec 28, 2000 10:31 AM
|
|
In response to the comment that Logicians have not shown the
non-existence of a program which can verify all proofs:
This, to my knowledge, is the Turing Halting Problem. It is usually
discussed in the context of Undecidable Languages. The theory was
developed in the 1930's with the intent of demonstrating the
impossibility of mechanized mathematical reasoning. If anyone is
interested in the subject or a proof that it is impossible for a
computer to verify all proofs, refer to Computation Complexity by
Papadimitriou. ISBN 0-201-53082-1.
In response to the comment about a computer checking Wile's Proof:
I agree, it is impossible for a computer to verify Wile's Proof as
written in English. The English proof would need to be translated
into a language the computer could understand. This would probably be
a tedious procedure; but in the end, we would know there isn't a
mistake. Of course, there could be errors in translating the machine
version back to English; but, these errors, in my opinion, would be
less problematic than those occurring in natural English proofs. At
least this way, we would be a little more certain of the veracity of a
given proof.
|
|
|
|
