Abstract
We contribute to the fully formal verification of Hales' proof of the Kepler Conjecure by analyzing the enumeration of all tame plane graphs. We sketch a formalization of plane graphs, tameness and Hales' enumeration procedure in Higher Order Logic. The correctness of the enumeration is partially verified (which uncovered a small mismatch between Hales' definition of tameness and his enumeration procedure). By executing the enumeration in ML we confirm that a list of plane graphs provided by Hales (the archive) contains all tame plane graphs (although it also contains much redundancy).
| Original language | English |
|---|---|
| Journal | Dagstuhl Seminar Proceedings |
| Volume | 5021 |
| State | Published - 2006 |
| Event | Mathematics, Algorithms, Proofs 2005 - Wadern, Germany Duration: 9 Jan 2005 → 14 Jan 2005 |