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.