- announcement of proof, July 1998
- early versions of proof, 1998 and 2002
- unabridged version of proof, 2005

- Java code, 1998
- Java code, 2002 (This file corrects a bug in the 1998 version, which caused a few graphs to be missed. It also contains linear programming code for tame graphs containing only triangles and quadrilaterals.)

- Samuel Ferguson's code
- Hales's code (1998)
- code additions (2002)
- code additions (2005)

- A 500MB file of everything related to linear programming. The tar file contains Mathematica code for generating the linear programs (CPLEX format) attached to a tame graph, the generated linear program files, the output files from running the linear programs, and log files describing how to control the branch-and-bound.

- Mathematica definitions of common functions used in the proof
- HOL Light specification of interval arithmetic inequalities
- Much of the original 1998 computer code can also be found in the source files of the first version of the proof.

Visit Hales's website for additional materials related to the proof of the Kepler conjecture.

Please report mistakes to Thomas Hales

.