Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)
Zoom in further on one ball's neighbourhood and draw a dot for each nearby ball and a line whenever two neighbours touch or are close; this sketch is a small graph drawn on a sphere around the ball, which can be flattened into the plane. Hales shows that if a packing is packed as densely as a counterexample would require, this little graph can only look like one of a very restricted set of shapes — never wildly irregular — which is what lets a computer take over the case-checking.
Compactness lets Hales assume a counterexample to the local annulus inequality has a special extremal form, called contravening. A detailed geometric study of a contravening (the 'main estimate') shows that its combinatorial pattern of nearby balls always forms a plane graph satisfying a short list of restrictive combinatorial conditions on vertex degrees and face sizes; such a graph is called tame. Every possible counterexample is thereby tagged with one specific tame plane graph, turning an analytic problem about ball positions into a finite combinatorial classification problem about graphs.
- tame plane graph
- A plane graph — vertices and edges drawn without crossings on a flat surface — is called tame if it satisfies a short, precise list of restrictions on how many edges meet at each vertex and how many sides each face has.