Loading ...
Sorry, an error occurred while loading the content.

[Computational Complexity] Computer-Assisted Proofs

Expand Messages
  • Lance
    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
    Message 1 of 1 , Mar 5, 2006
    • 0 Attachment
      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.

      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.

      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?

      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

    Your message has been successfully submitted and would be delivered to recipients shortly.