Kepler Conjecture

The Kepler conjecture (Kepler 1611) asserts that close packing (either cubic or hexagonal close packing, both of which have maximum densities of ) is the densest possible sphere packing. Finding the densest (not necessarily periodic) packing of spheres is known as the Kepler problem.

Buckminster Fuller (1975) claimed to have a proof, but it was really a description of face-centered cubic packing, not a proof of its optimality (Sloane 1998). A second putative proof of the Kepler conjecture was put forward by W.-Y. Hsiang (Cipra 1991, Hsiang 1992, 1993, Cipra 1993), but was subsequently determined to be flawed (Conway et al. 1994, Hales 1994, Sloane 1998). According to J. H. Conway, nobody who has read Hsiang's proof has any doubts about its validity: it is nonsense.

Soon thereafter, Hales (1997a) published a detailed plan describing how the Kepler conjecture might be proved using a significantly different approach from earlier attempts and making extensive use of computer calculations. Hales subsequently completed a full proof, which appears in a series of papers totaling more than 250 pages (Cipra 1998). A broad outline of the proof in elementary terms appeared in Hales (2002). The proof relies extensively on methods from the theory of global optimization, linear programming, and interval arithmetic. The computer files containing the computer code and data files for combinatorics, interval arithmetic, and linear programs require more than 3 gigabytes of space for storage.

Hales' proof proved difficult to verify. In 2003, it was reported that the Annals of Mathematics publication would have an unusual editorial note stating that parts of the paper have not been possible to check, despite the fact that a team of 12 reviewers worked on verifying the proof for more than four years and that the reviewers were 99% certain that it is correct (Holden 2003, Szpiro 2003). However, the actual publication contains no such note (Hales 2005).

In response to the difficulties in verifying his proof, in January of 2003, Hales launched the "Flyspeck project" ("Formal Proof of Kepler") in an attempt to use computers to automatically verify every step of the proof. The project, believed by Hales at its inception to require 20 person-years of labor (Holden 2003, Szpiro 2003), was officially completed on Aug. 10, 2014. The formalization used HOL Light and Isabelle and covered both the mathematical text and the computer calculations. The complete published account is Hales et al. (2017).