Kepler's Conjecture Theorem

Kepler's conjecture, one of the oldest conjectures in geometry, was that the optimal packing of unit spheres could never achieve a density of more than pi/sqrt{18}. A few years ago, Thomas Hales (with help from Samuel Ferguson), proved the conjecture with extensive use of computers to assist in the proof. The New York Times, in their infiinte wisdom, managed to greet this proof with a line that went something like 'Mathematicians have now proved what greengrocers have known all long' ....sigh...

What prompted this note is a new article (NYT; reg. reqd) that indicates that Thomas Hales' proof is going to be split into two parts:

But Dr. Hales's proof of the problem, known as the Kepler Conjecture, hinges on a complex series of computer calculations, too many and too tedious for mathematicians reviewing his paper to check by hand.

Believing it thus, at some level, requires faith that the computer performed the calculations flawlessly, without any programming bugs. For a field that trades in dispassionate logic and supposedly unambiguous truths and falsehoods, that is an uncomfortably gray in-between.

Because of the ambiguities, the journal, the prestigious Annals of Mathematics, has decided to publish only the theoretical parts of the proof, which have been checked in the traditional manner. A more specialized journal, Discrete and Computational Geometry, will publish the computer sections.


Now I don't quite trust the NYT when it comes to matters of science, but if this is true, it does send a rather unpleasant message, that the Annals of Mathematics is the place for rigorous proofs, and Discrete and Computational Geometry is the place for "computer-assisted proofs" (you can almost hear the sneer in that line). Now D&CG is the one of the primary journals of reference for work in computational geometry, and most of the papers published there are as theoretical as any. So I am somewhat puzzled at why this decision was made. If someone has more information to share, I'd like to hear more about it.