Kepler's sphere-packing conjecture

In three-dimensional space, consider packings of congruent non-overlapping spheres, and let their density be the proportion of space occupied by the spheres, interpreted as the asymptotic density of the packing. Kepler's conjecture. The maximal density of sphere packings in three-dimensional space is

$$\frac{\pi}{\sqrt{18}}.$$

The conjecture was stated by Johannes Kepler in 1611 and was proved by Thomas Hales, including a formal verification project, so the claim is solved.