SourceForge.net Logo
project summary

 

Flyspeck I: Tame Graphs

Title: Flyspeck I: Tame Graphs
Author: Gertrud Bauer and Tobias Nipkow
Submission date: 2006-05-22
Abstract: These theories present the verified enumeration of tame plane graphs as defined by Thomas C. Hales in his proof of the Kepler Conjecture in his book Dense Sphere Packings. A Blueprint for Formal Proofs. [CUP 2012]. The values of the constants in the definition of tameness are identical to those in the Flyspeck project. The IJCAR 2006 paper by Nipkow, Bauer and Schultz refers to the original version of Hales' proof.
Change history: [2010-11-02]: modified theories to reflect the modified definition of tameness in Hales' revised proof.
[2014-07-03]: modified constants in def of tameness and Archive according to the final state of the Flyspeck proof.
BibTeX:
@article{Flyspeck-Tame-AFP,
  author  = {Gertrud Bauer and Tobias Nipkow},
  title   = {Flyspeck I: Tame Graphs},
  journal = {Archive of Formal Proofs},
  month   = may,
  year    = 2006,
  note    = {\url{http://afp.sf.net/entries/Flyspeck-Tame.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License