The Kepler Conjecture

1953: Laszlo Feje Toth proves that the number of cases to be checked in order to prove Kepler’s Conjecture is finite.

1998: The Kepler Conjecture (now – a theorem) is proved by exhaustion: The review panel declares a “99% certainty” the proof is valid.

2003: Project Flyspeck aims to make computer-based proof to be accepted as valid proof.

2014: The project is completed successfully.

2016: The conjecture is proven in 8 dimensions and in 24 dimensions.

• The Face-centered hexagonal packing of equal spheres and the face centered cubicpacking have the same densitiy ~74.05%. This is a lower bound.
• 1611: Kepler’s Conjecture: The maximal density of 3-d packing of equally sized spheres, is 74.05%.
• 1900: Hilbert presented 23 unsolved problems. No. 18 is Kepler’s conjecture.
• 1993: Muder proved that the density cannot exceed 77.31%. This is an upper-bound. However, he did not demonstrate a packing with that density.

Areas and volumes  (MSC2010#97G30)

• Surface area and volume of a sphere
• Cubic/Hexagonal packing

Logic (MSC2010#97E30)

• Computer-assisted proof
• Computerized verification of proofs

Geometry (MSC2010#97G99)

• Discrete-Computational geometry