Well, proofs are recursively enumerable, so if there is a proof, a machine can (eventually, but not necessarily practically) find it. And if you restrict your proofs to some maximum length, then it is computable whether or not a "not-too-long" proof exists. I think the real problem is proving that what you ask a machine to prove is a correct translation of what you actually meant. This is a similar problem to proving programs correct--the description of what it means to be correct may not match what the program is really supposed to do. --ms On 9/30/2011 10:50 AM, Henry Baker wrote:
Not true. All legitimate proofs are machine-checkable, but coming up with such a proof is a non-computable exercise.
Now a machine-checkable proof may be a bit more tedious to read, just as reading machine code is more tedious than reading C/Lisp/Java/whatever, because every bit of detail must be written out. However, once such a project gets off the ground, the large number of little lemmas required will eventually be already incorporated into such a Wikipedia, enabling reasonably short machine-checkable proofs to be expressed.
At 07:36 AM 9/30/2011, Adam P. Goucher wrote: Machines cannot check general mathematical proofs, due to Gödel's
Incompleteness Theorem. Indeed, if they could, mathematicians would quickly be rendered obsolete, as a computer could soon perform a breadth-first search of proofs.
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun