The Proof That Took 400 Years and a Computer

In 1611, Johannes Kepler tossed off a guess in a New Year's gift pamphlet for his patron called On the Six-Cornered Snowflake: stack cannonballs the way a greengrocer stacks oranges, and you cannot do better. No arrangement of equal spheres fills space more densely than the face-centered cubic.

Proving it took until August 1998. Thomas Hales, then at the University of Michigan, submitted a 250-page argument backed by three gigabytes of computer code. The strategy: reduce the infinite question to a finite one — about 5,000 candidate sphere configurations — then beat each one with linear programming, roughly 100,000 problems in all. His student Sam Ferguson did the worst of them.

The Annals of Mathematics sent it to twelve referees and gave them four years. In 2003, panel head Gábor Fejes Tóth came back with a verdict no one had heard before: 99 percent sure it's correct, but we cannot check the computer parts. The journal published the human-readable hundred pages in 2005 with that asterisk attached.

Hales did not enjoy the asterisk. In January 2003 he launched the Flyspeck project — "Formal Proof of Kepler" — to translate every step into a machine-checkable proof using HOL Light and Isabelle, two automated proof assistants that accept nothing on faith. He estimated twenty person-years.

It finished on August 10, 2014. The conjecture Kepler scribbled while thinking about snowflakes is now one of the most thoroughly verified theorems in mathematics, by some distance.