If a putative proof is then put into official proof format, as defined by logicians, then -- assuming sufficient computing resources -- checking it should be a piece of cake. (Each statement in sequence must be either
1) an axiom or
2) a statement B such that statements A, and A => B, are prior statements in the proof,
and the last statement is what was to be proved.)
Do you have any idea how far published mathematical proofs are from this level? I would guess that a typical published proof would require millions or even billions of statements. So any such project would have to operate at a higher level than that. And now you come to another problem: groundbreaking results, and a large fraction of those that aren't groundbreaking, involve the introduction of one or more new ideas. And those ideas would have to be introduced to the proof machinery before it could verify the result - at which point the utility of the exercise is very much in question. ___________________________________________________ Try the New Netscape Mail Today! Virtually Spam-Free | More Storage | Import Your Contact List http://mail.netscape.com