Kepler conjecture

In three-dimensional Euclidean space, no arrangement of equal, non-overlapping spheres has a density greater than $\pi/\sqrt{18} \approx 0.74048$, the density of the face-centered cubic and hexagonal close packings — the familiar way grocers stack oranges or cannonballs.

Hales announced a proof in 1998 (with Samuel Ferguson) combining a classical reduction to finitely many local configurations with an exhaustive computer search — linear-programming bounds checked on roughly 5,000 cases. A panel of twelve referees reported in 2003 that they were "99% certain" the proof was correct but could not verify every computer calculation by hand, so the Annals of Mathematics published it in 2005 with that caveat noted. The Flyspeck project, led by Hales, then built a complete formal proof checked line by line by the HOL Light and Isabelle proof assistants, removing the remaining doubt; Flyspeck was announced complete in 2014, and the formal proof was published in 2017.