On that note, Metamath (http://us.metamath.org) has actually gone ahead and done a lot of this work. It fully develops group, field, ring, and vector space theory from ZFC, and also has a complete construction of the real and complex numbers included. It's very cool: you should check it out. -Scott On Fri, Sep 30, 2011 at 10:50 AM, Henry Baker <hbaker1@pipeline.com> 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