[skermes]

This question came up in some of my more abstract classes in college. A few professors in my department were working on slightly different problems in the same general domain of automated mathematical problem solving and proof construction. The general consensus as I remember it was that the simplest way to get around the problem of no human being able to survey these proofs was to do something like this:

1. Define a machine read- and writable logic that can express your theorem and the steps you think it'll take to get there. 2. Write an automated proof-checker that can verify that proofs in this language are correct. 3. Prove the correctness of the checker. 4. Write a program that starts with your axioms and writes out a proof that ends in your theorem. 5. Verify it with the checker.

Now the only proof that needs to be human-surveyable for us to be certain that everything is correct is the one in step 3. The proof created by step 4 can fill up a skyscraper full of hard disks, and as long as the proof checker verifies it we know that it must be correct. Given a simple enough proof language (FOPL, for example) and a suitable programming language (the choice at the time was lisp, I believe) step 3's proof is easily short enough for a human to verify.

The only hole left is the possibility of a subtle machine malfunction that causes the checker to falsely categorize a proof as correct. On modern hardware this possibility is remote enough that once a proof has been verified a number of times by independent researchers on their own hardware we can safely ignore it.

[Dove]

Reminds me of discussions which purported to prove, not that a particular number was prime, but that there was a 1 in BigNum probability that it was not prime.

The mathematicians in the audience seemed to consider that unacceptable to the point of being useless. Nonetheless, someone pointed out (to much laughter) that the chances of any given proof being incorrect were significantly higher than that 1 in BigNum. Of course, we've all been there--thought we proved something we didn't.

I regard the chances of machine malfunction similarly, and have a similar standard for proof. If you can examine the code and the processes sufficiently, there is no reason not to trust the machine. At least, no more reason than there is not to trust your and others' minds. I suspect this view is common, given that most folks consider the Four Color Theorem proven.

[vilya]

This looks like a good time to quote Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

[vinutheraj]

Yes, exactly, what if the thing they proved is not what they coded in the end, there is a good enough probability of bugs if the code is sufficiently big !