Computers Verify Correctness of Kepler Conjecture Proof

Formal proof software assistants have verified the correctness of Thomas Hales's 1998 proof of the Kepler conjecture.

Hales's proof, what New Scientist calls "a 300-page monster that took 12 reviewers four years to check for errors," was published in Annals of Mathematics in 2005, but with the caveat that reviewers were only "99 percent certain" it was correct.

Now, though, the computers have removed the referees from the equation. Says Hale:

This technology cuts the mathematical referees out of the verification process. Their opinion about the correctness of the proof no longer matters.

Read New Scientist's coverage.