Materials for the proof of the Kepler Conjecture.
The Kepler Conjecture asserts that no packing of congruent balls in Euclidean space has density greater than the density of the face-centered cubic packing.
The Kepler Conjecture was proved by Sam Ferguson and Tom Hales in 1998. it was not published in full until 2006. An ongoing project, called Flyspeck, seeks to give a formal proof of the Kepler Conjecture.
Current Materials
Legacy Materials - The 1998 website on the proof of the Kepler conjecture
- The original source code for the 1998 proof (tar files cached at the Math ArXiv).
- The original source code for the 1998 proof, 2002 revision, 2004 revision (indexed by Google code, stored at Pitt).
- The original 1998 web pages on the proof.
- The abridged proof appearing in the Annals of Mathematics in 2005. (This link includes a copy of the computer code used in the proof. However, this is not the best place to download the software, because it hasn't been maintained since 2005.)
- The unabridged proof appearing in Discrete and Computational Geometry in 2006.
- An unfinished book from 2008 "Flyspeck: A Blueprint for the Formal Proof of the Kepler Conjecture"
- A collection "Lemmas in Elementary Geometry" from 2008. (Results in the Tarski arithmetic.)
|
|