Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)
Picture stacking oranges at a grocery store: the pyramid shape everyone uses, called the face-centred cubic packing, fills about of space. In 1611 Kepler guessed that no arrangement of equal balls, however clever, can ever beat this — but 'no arrangement, ever' is an infinite claim about infinitely many possible packings, so nobody could check it by hand. The plan of this proof is to shrink that infinite claim down to a finite, mechanical checklist that a computer program can run through and a proof assistant can certify line by line.
A packing is an infinite discrete set of unit-ball centres with every two points at distance at least ; its density is a limit of the fraction of a large container that the balls fill. Kepler's booklet 'On the Six-Cornered Snowflake' (1611) conjectured that this density never exceeds , the value attained by the face-centred cubic packing and by uncountably many other packings built from the same hexagonal layers. Thomas Hales and Samuel Ferguson proved the conjecture in 1998 through geometric case analysis combined with extensive computer calculation, but as Jeffrey Lagarias reported after chairing the referee panel, the proof's nature 'makes it hard for humans to check every step reliably,' and it was published in 2006 without full certification.
Hales's response, announced in 2003, was the Flyspeck project (Formal Proof of the Kepler conjecture): re-derive every part of the argument — both the traditional mathematical text and the parts implemented as computer calculations — inside the HOL Light and Isabelle proof assistants, so that a small, heavily scrutinised logical kernel checks each deduction instead of a human referee. The project closed in 2014 and the official account was published by Hales and twenty-one coauthors in 2017.
The remaining steps of this proof sketch follow the paper's own outline: reduce the infinite geometric problem to finitely many combinatorial cases (Steps 2–3), turn the numerical part of each case into inequalities that can be certified by pure arithmetic (Steps 4–7), and assemble the certified pieces into the final formal theorem (Step 8).
- packing and density
- A packing is a way of placing non-overlapping unit balls in space by choosing their centres ; the density is the fraction of a huge region that the balls fill, in the limit as the region grows.
- proof assistant (formal proof)
- A proof assistant such as HOL Light or Isabelle is a computer program that only accepts a deduction if it follows from a tiny, fixed set of logical axioms and inference rules, so a proof it certifies is checked with the reliability of arithmetic rather than human review.