Towards a Verified Enumeration of All Tame Plane Graphs

Authors Tobias Nipkow, Gertrud Bauer

Thumbnail PDF


  • Filesize: 327 kB
  • 25 pages

Document Identifiers

Author Details

Tobias Nipkow
Gertrud Bauer

Cite AsGet BibTex

Tobias Nipkow and Gertrud Bauer. Towards a Verified Enumeration of All Tame Plane Graphs. In Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, Volume 5021, pp. 1-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)


In his proof of the Kepler conjecture, Thomas Hales introduced the notion of tame graphs and provided a Java program for enumerating all tame plane graphs. We have translated his Java program into an executable function in HOL ("the generator"), have formalized the notions of tameness and planarity in HOL, and have partially proved that the generator returns all tame plane graphs. Running the generator in ML has shows that the list of plane tame graphs ("the archive") that Thomas Hales also provides is complete. Once we have finished the completeness proof for the generator. In addition we checked the redundancy of the archive by formalising an executable notion of isomorphism between plane graphs, and checking if the archive contains only graphs produced by the generator. It turned out that 2257 of the 5128 graphs in the archive are either not tame or isomorphic to another graph in the archive.
  • Kepler conjecture
  • certified proofs
  • flyspeck


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads