--- Henry Baker <hbaker1@pipeline.com> wrote:
Computer proof-checking technology (HW & SW) have gotten to the point where it now makes sense to develop a system whereby _every_ mathematical proof could eventually be _checked_ by computer. This won't happen overnight, but will require a 10-20 year effort to develop a generic system into which one could shovel all the lemmas, theorems, etc., so that _every_ paper submitted to a math journal would come with its own certification that the proof is valid.
Such a computer program would be as intricate as the proofs it is expected to verify, and is subject to the same human error. There cannot be certainty of correctness of a proof without certainty of the correctness of the proof-checking software. Could the program check itself? Gene __________________________________________________ Do You Yahoo!? Tired of spam? Yahoo! Mail has the best spam protection around http://mail.yahoo.com