Towards a Verified Enumeration of All Tame Plane Graphs
Tobias Nipkow, Gertrud Bauer · 2005
We contribute to the fully formal verification of Hales' proof of the Kepler Conjecure by analyzing the enumeration of all tame plane graphs. We sketch a formalization of plane graphs, tameness and Hales' enumeration procedure in Higher Order Logic. The correctness of the enumeration is partially verified (which uncovered a small mismatch be- tween Hales' definition of tameness and his enumeration procedure). By executing the enumeration in ML we confirm that a list of plane graphs provided by Hales (the archive) contains all tame plane graphs (although it also contains much redundancy).