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.

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.