Worked solution: Flyspeck: a formal proof of the Kepler conjecture in HOL Light and Isabelle (2015)
Since only a restricted family of shapes can occur, a computer can simply try to draw every possible one, throwing away any half-built shape that has already broken a tameness rule, much like solving a jigsaw puzzle by rejecting pieces that don't fit as soon as they're tried. The output is a finite gallery of graphs, and the hard mathematical claim is that this gallery is complete — nothing is missing.
A computer search enumerates all finite plane graphs satisfying the tameness conditions, pruning branches that can never become tame; the resulting archive — originally more than graphs, later refined to once the tameness definition was sharpened for formalisation — is proved complete: every tame plane graph is isomorphic to one on the list. This completeness theorem was formalised in Isabelle/HOL (the enumeration explores on the order of intermediate graphs) and then imported into HOL Light as a hand-translated assumption; because every quantifier in the statement ranges over a bounded, finite structure, the statement is equivalent to a propositional satisfiability claim that is provable identically in either logic, which is what justifies moving it across proof assistants.
- isomorphic graphs
- Two graphs are isomorphic if one can be relabelled to look exactly like the other — same vertices, same edges, same connections — even if they are drawn differently on the page.