Computer resources for the Kepler conjecture
Documents
Computer code for graph generation
- 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.)
Interval arithmetic code
Computer code for linear programming
- 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.
Miscellaneous code
- 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
.