Flyspeck I: Tame Graphs

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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. Automated Reasoning, 21–35. https://doi.org/10.1007/11814771_4
Nipkow, T. (2011). Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism. Interactive Theorem Proving, 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

Session Flyspeck-Tame-Computation

Depends on

Trie