In 1611, Kepler proposed that close packing (either cubic or hexagonal close packing, both of which
have maximum densities of ) is the densest possible sphere
packing, and this assertion is known as the Kepler conjecture. 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 completed in 2014.
) is the densest possible sphere
packing, and this assertion is known as the Kepler conjecture. Finding the densest
(not necessarily periodic) packing of spheres is known as the Kepler
problem.
