Hales' detailed proof of Kepler's conjecture, in Disc. Comp. Geom.

Readers of this blog will be well aware of the interesting events surrounding Thomas Hale's proof of Kepler's conjecture:

...that close packing (either cubic or hexagonal close packing, both of which have maximum densities of ) is the densest possible sphere packing

In short, his proof involved large amounts of computer verification, and after three years of intensive effort, the Annals of Mathematics determined that it could not verify with certainty that the proof was correct (not because there were problems, but because the proof had many "low-level components" that lacked a more general intuition, and were thus hard to verify, especially given the degree of computer search involved).

A strange arrangement was then made: the Annals of Mathematics published a briefer version of the proof, and made the code/data for the proof available unreviewed on its website. Discrete and Computational Geometry then undertook to publish detailed versions of the six preprints that Hales and his student S. P. Ferguson wrote in 1998.

That issue is now out, with a foreword by Gabor Fejes-Toth (who ran the committee that first attempted to verify the conjecture for Ann. Math) and Jeff Lagarias (much-missed AT&T alum who spent a significant amount of time and effort restructuring and clarifying the proofs from the original preprints.

Categories:

• kepler-conjecture