| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
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 revised proof of the Kepler Conjecture. The revison concerns the definition of tameness. 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. |
| 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},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|