Thomas C. Hales talk at the recent AAAS meeting about his proof of the Kepler conjecture. From a New Scientist item In 1998 Hales submitted a computer-assisted proof of the Kepler conjecture, a theorem dating back to 1611. This describes the most efficient way to pack spheres in a box, wasting as little space as possible. It appears the best arrangement resembles the stacks of oranges seen in grocery stores.

Should we trust such a computer-assisted proof? I have more faith in a computer properly executing its code more than a mathematician verifying a proof. But what should constitute a legitimate proof when part of that proof is verified by a computer?Hales' proof is over 300 pages long and involves 40,000 lines of custom computer code. When he and his colleagues sent it to the Annals of Mathematics for publication, 12 reviewers were assigned to check the proof. "After four years they came back to me and said they were 99% sure that the proof was correct and they said were they exhausted from checking the proof," Hale says.

As a result, the journal then took the unusual step of publishing the paper without complete certification from the referees.

In most mathematical papers, we don't give formal logical proofs of our theorems. Instead we give a detailed proof that gives all of the necessary ideas to convince the reader that a formal proof would be possible. But, at least with our current technology, that level of informality will not work with computer code. So any proof using computer verification should have a formal proof of the correctness of the code.

This would require significant work from the author, but we are talking about establishing mathematical truths. When the other alternative is publishing the solutions to major open questions without being fully refereed, what choice do we have?

--

Posted by Lance to Computational Complexity at 3/05/2006 09:32:00 AM