Hales work on Kepler conjecture

Question

It seems that the Fulkerson prize has been attributed to Thomas Hales for this work. What is the present status of the conjecture, then?

Answer 1

The original 1998 proof appeared in 2005/6, in an abridged version in Annals of Mathematics:

A proof of the Kepler conjecture. Ann. of Math. (2) 162 (2005), no. 3, 1065–1185.

and unabridged as volume 36 of Discrete & Computational Geometry (2006).

It is my understanding that meanwhile there are no actual doubts in this proof (though, possibly, still some reservations by some, due to the complexity and the computer aid).

Thus, there is an ongoing effort to simplfy/clean up/formalize the proof. For example:

Hales, Thomas C.; Harrison, John; McLaughlin, Sean; Nipkow, Tobias; Obua, Steven; Zumkeller, Roland "A revision of the proof of the Kepler conjecture" Discrete Comput. Geom. 44 (2010), no. 1, 1–34.

From the MR review of that paper (by Uwe Schnell):

Since the original proof makes use of computer programs, the so-called Flyspeck project was started to give a formal proof of the Kepler conjecture. This article summarizes the current status of this initiative and gives a list of minor errata in the original proof.

Regarding this Flyspeck project see for example a recent presentation by Hales (given March 2012, the date on the slides seems wrong), where he says that this project is 80% complete. On the web one can easily find further information related to this project.

Update: The Flyspeck program was completed in August 2014. See this Announcement

---

OP asks regarding the meaning of the awarding of the Fulkerson prize:

In some sense there is no specific meaning to it (as concerns acceptance of the community of the proof) as the Fulkerson prize is not a prize that is a priori awarded for 'The Kepler Conjecture', as opposed to the situation, say, for the Wolfskehl prize for FLT or the Clay prizes for the seven problems. By contrast 'The Delbert Ray Fulkerson Prize recognizes outstanding papers in the area of discrete mathematics.' So that in principle it would even be possible that the prize would be awarded while people only believe that the papers make significant progress towards a proof. However, this seems not the case as the Notices AMS article on the 2009 awarding of this prize contains 'After four centuries, Ferguson and Hales have now proven Kepler’s assertion.' Thus, yes, this is further evidence that the proof is generally accepted.

However, also note that this was not the first prize they received for their work. They also received the 2007 Robbins prize. The citation contains "The Kepler conjecture asserts [...] The proof of this result is a landmark achievement." but also at the end "Some controversy has surrounded this proof, with its large computer component, concerning its reliable checkability by humans. Addressing this issue, Hales has an ongoing project, called the 'Flyspeck' project, whose object is to construct a 'second-generation' proof which is entirely checkable by computer in a formal logic system."

So, in summary, this prize is a recognition of their work and that it was awarded can be considered as further evidendence that the proof is accepted as correct. However, I would not consider the awarding of this prize as something like the moment when the proof in any sense 'officially' got accepted as such. (Indeed, as far as I know, it was already widely accepted several years before that, e.g., otherwise the Annals would not have published this paper; except for the reservations I mentioned above, but then those also did not get addressed by the prize-awarding.)