# What programing language Thomas Hales used in 1998 to prove Kepler’s conjecture?

Mathematicians have been studying sphere packings since at least 1611, when Johannes Kepler conjectured that the densest way to pack together equal-sized spheres in space is the familiar pyramidal piling of oranges seen in grocery stores. Despite the problem’s seeming simplicity, it was not settled until 1998, when Thomas Hales finally proved Kepler’s conjecture in 250 pages of mathematical arguments combined with mammoth computer calculations (3 gigabytes of computer programs, data and results).

What programing language Thomas Hales used in 1998 to prove Kepler’s conjecture?

• Does it not say in his published paper(s)? Mar 31 '16 at 10:59
• (I've given up searching through his papers. The link to the computer part of the proof should be: annals.math.princeton.edu/keplerconjecture but it is a dead link.) Mar 31 '16 at 11:09
• @user1729 I have not fond any info.
– iLie
Mar 31 '16 at 11:19

The code that you are looking for is pointed to in Hales's paper Sphere packings I, but the link given therein is no longer valid; the currently valid link is on GitHub and, in Hales's own words, is a combination of C++, Java and Mathematica.

The answer given by Raymond Manzoni is not correct: he refers to a later project, in which Hales used different programming languages to formally check the validity of his original proof

• Thank you, you are right. Good link.
– iLie
Mar 31 '16 at 11:34

Warning As pointed by Alex M. This answer concerns a revision of the project and not the $1998$ version (sorry for that...)

Details of the software environment used are in Hales' "A formal proof of the Kepler conjecture" paper (while the Ams paper/book is here) :

"The code and documentation for the Flyspeck project are available at a Google code repository devoted to the project 7. The parts of the project that have been carried out in Isabelle are available from the Archive of Formal Proofs ( afp.sf.net ). Other required software tools are Subversion (for interactions with the code repository), Isabelle/HOL 37, HOL Light 21, OCaml (the implementation language of HOL Light), the CamlP5 preprocessor (for a syntax extension to OCaml for parsing of mathematical terms), and GLPK (for linear programming) 8."

• The OP was asking about the 1998 proof, which used C++, Java and Mathematica. What you mention is a later project of the same author. Mar 31 '16 at 11:30
• @Alex M(+1) Sorry for that... Should I erase this answer or may it be useful for future work? Mar 31 '16 at 11:34
• Don't erase it, it still provides useful information and together with my answer a reader might get a better view on the subject. Mar 31 '16 at 11:35