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?
 A: 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."
A: 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
