Flyspeck I: Tame Graphs

Tobias Nipkow, Gertrud Bauer, Paula Schultz†

We present a verified enumeration of tame graphs as defined in Hales' proof of the Kepler Conjecture and confirm the completeness of Hales' list of all tame graphs while reducing it from 5128 to 2771 graphs.

ps pdf SpringerLink

Isabelle theories (outline, pdf)
Isabelle theories (full, pdf)
Isabelle theories (full, html)

Archive: Tri Quad Pent Hex Hept Oct

BibTeX:

@inproceedings{NipkowBS-IJCAR06,
  author={Tobias Nipkow and Gertrud Bauer and Paula Schultz},
  title={Flyspeck {I}: Tame Graphs},
  booktitle="Automated Reasoning (IJCAR 2006)",
  editor="U. Furbach and N. Shankar",
  publisher=Springer,series=LNCS,volume={4130},pages={21--35},year=2006
}