Kepler conjecture

The Kepler conjecture, named after the 17th-century mathematician and astronomer Johannes Kepler, is a mathematical theorem about sphere packing in three-dimensional Euclidean space. It states that no arrangement of equally sized spheres filling space has a greater average density than that of the cubic close packing (face-centered cubic) and hexagonal close packing arrangements. The density of these arrangements is around 74.05%. In 1998, Thomas Hales, following an approach suggested by , announced that he had a proof of the Kepler conjecture. Hales' proof is a proof by exhaustion involving the checking of many individual cases using complex computer calculations. Referees said that they were "99% certain" of the correctness of Hales' proof, and the Kepler conjecture was accepted as a theorem. In 2014, the Flyspeck project team, headed by Hales, announced the completion of a formal proof of the Kepler conjecture using a combination of the Isabelle and HOL Light proof assistants. In 2017, the formal proof was accepted by the journal Forum of Mathematics, Pi. Background Imagine filling a large container with small equal-sized spheres: Say a porcelain gallon jug with identical marbles. The "density" of the arrangement is equal to the total volume of all the marbles, divided by the volume of the jug. To maximize the number of marbles in the jug means to create an arrangement of marbles stacked between the sides and bottom of the jug, that has the highest possible density, so that the marbles are packed together as closely as possible.