Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism

Tobias Nipkow

Due to a recent revision of Hales's proof of the Kepler Conjecture, the existing verification of the central graph enumeration procedure had to be revised because it now has to cope with more than $10^9$ graphs. This resulted in a new and modular design. This paper primarily describes the reusable components of the new design: a while combinator for partial functions, a theory of worklist algorithms, a stepwise implementation of a data type of sets over a quasi-order with the help of tries, and a plane graph isomorphism checker. The verification turned out not to be in vain as it uncovered a bug in Hales's graph enumeration code.


author={Tobias Nipkow},
title={Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism},
booktitle={Interactive Theorem Proving (ITP 2011)},
editor={van Ekelen and Geuvers and Schmaltz and Wiedijk},