Collaborative Mathematics and Kepler's conjecture/theorem

If the 1990s was the decade of the web, the 2000s might very well be the decade of collaborative methods, whether it be social bookmarking, tagging, or recommendation systems. A collaborative system we possibly did not anticipate is combined theorem proving.

Kepler's conjecture about the optimal packing of balls in 3D was finally proved by Thomas Hales in 1998. Or was it ? Since 1999, a 12-member review committee of the Annals of Mathematics has been going over the proof in order to verify it. The NYT reported nearly two years ago that there were problems in the verification process, and now we hear the details, on Thomas Hales' Flyspeck page:

Robert MacPherson, editor of the Annals, wrote a report that states

``The news from the referees is bad, from my perspective. They have not been able to certify the correctness of the proof, and will not be able to certify it in the future, because they have run out of energy to devote to the problem. This is not what I had hoped for.''

Interestingly, Gabor Fejes Tóth, the chief referee, wrote a report certifying that he was "99%" confident of the proof, but no more, and the editor therefore concluded that

it's not enough for complete certification as correct, for two reasons. First, rigor and certainty was what this particular problem was about in the first place. Second, there are not so many general principles and theoretical consistencies as there were, say, in the proof of Fermat, so as to make you convinced that even if there is a small error, it won't affect the basic structure of the proof.''

Apparently, the Annals will publish a paper on this topic with a disclaimer stating that the computer parts of the proof have not been verified. In the meantime, (and here's the collaborative aspect of this), Thomas Hales and others have undertaken a joint effort to rewrite his proof in a computer-verifiable form using OCAML. The project is called Flyspeck, and the page contains information on how to "participate" in the proof:

The first step is to learn the relevant background material:

• Objective CAML,
• HOL light, and
• the idea of the proof of the Kepler Conjecture.

See the resources listed at the bottom of the page for more information about these topics.

The second step is to become an experienced user. In practical terms, this means being able to create your own proof in the HOL light system.

If you have successfully proved a non-trivial theorem in the HOL light system, then contact Thomas C. Hales (http://www.math.pitt.edu/~thales) if you wish to participate.

(HT: sigfpe)