### 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, the ITP 2011 paper by Nipkow refers to the Blueprint version of the proof.

### License

BSD License

### History

July 3, 2014
  modified constants in def of tameness and Archive according to the final state of the Flyspeck proof.
November 2, 2010
  modified theories to reflect the modified definition of tameness in Hales' revised proof.

### Topics

- Mathematics/Graph theory

### Related publications

- Nipkow, T., Bauer, G., & Schultz, P. (2006). Flyspeck I: Tame Graphs. Lecture Notes in Computer Science, 21–35. https://doi.org/10.1007/11814771_4
- Nipkow, T. (2011). Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. Lecture Notes in Computer Science, 281–296. https://doi.org/10.1007/978-3-642-22863-6_21
- Hales, T. C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., & Zumkeller, R. (2009). A Revision of the Proof of the Kepler Conjecture. Discrete & Computational Geometry, 44(1), 1–34. https://doi.org/10.1007/s00454-009-9148-4
- HALES, T., ADAMS, M., BAUER, G., DANG, T. D., HARRISON, J., HOANG, L. T., KALISZYK, C., MAGRON, V., MCLAUGHLIN, S., NGUYEN, T. T., NGUYEN, Q. T., NIPKOW, T., OBUA, S., PLESO, J., RUTE, J., SOLOVYEV, A., TA, T. H. A., TRAN, N. T., TRIEU, T. D., … ZUMKELLER, R. (2017). A FORMAL PROOF OF THE KEPLER CONJECTURE. Forum of Mathematics, Pi, 5. https://doi.org/10.1017/fmp.2017.1

### Session Flyspeck-Tame

- ListAux
- Quasi_Order
- PlaneGraphIso
- Rotation
- Graph
- IArray_Syntax
- Enumerator
- FaceDivision
- RTranCl
- Plane
- Plane1
- GraphProps
- EnumeratorProps
- FaceDivisionProps
- Invariants
- PlaneProps
- ListSum
- Tame
- Plane1Props
- Generator
- TameProps
- TameEnum
- ScoreProps
- LowerBound
- GeneratorProps
- TameEnumProps
- Worklist
- Maps
- Arch
- ArchCompAux
- ArchCompProps
- Relative_Completeness

### Session Flyspeck-Tame-Computation

- ArchComp
- Completeness

### Depends on

- Trie

### Auto-related entries

- The Myhill-Nerode Theorem Based on Regular Expressions

## Cite

×

Flyspeck-Tame-AFP

    @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{https://isa-afp.org/entries/Flyspeck-Tame.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 17, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 2, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 25, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jun 30, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Apr 29, 2009 : Isabelle2009
- Jun 10, 2008 : Isabelle2008
- Jan 4, 2008 : Isabelle2007
- Nov 27, 2007 : Isabelle2007