Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)
Instead of trying to think about all of infinite space at once, Hales zooms in on one ball at a time and looks only at its immediate neighbours, out to a fixed distance. If he can show that this small neighbourhood can never be too crowded, and every neighbourhood in the whole packing obeys the same local rule, then the whole infinite packing is controlled — like proving a whole orchard is healthy by checking that every single tree, plus its closest neighbours, looks fine.
Hales partitions space into Marchal cells and reduces the density bound to a local annulus inequality for centres with . The separation condition between distinct centres gives a packing bound of at most centres in this annulus; compactness then makes the resulting finite optimisation problems well posed. Thus the infinite geometric problem is reduced to finitely many local configurations.
- Marchal cell
- A region of space assigned to each ball centre so that the cells tile all of space without gaps or overlaps, built so that a ball's local crowding can be measured by the volume of its own cell.