Thomas Hales
fl. 1958, San Antonio, Texas, United States
American mathematician who proved the Kepler conjecture on sphere packing in 1998 and later led the Flyspeck project, a full formal, computer-verified version of the proof.
Thomas Hales was born in San Antonio, Texas, studied at Stanford University and Cambridge, and earned his PhD at Princeton University in 1986 under Robert Langlands, working on the Langlands programme. He taught at Harvard, the University of Chicago, and the Institute for Advanced Study before joining the University of Michigan in 1993.
In 1998, building on a strategy proposed by László Fejes Tóth in 1953, Hales and his graduate student Samuel Ferguson proved the Kepler conjecture: that face-centred cubic and hexagonal close packing achieve the densest possible packing of equal spheres in space, a claim Kepler had made in 1611. The proof combined classical analysis with roughly 300 pages of argument and gigabytes of computer calculation reducing the problem to thousands of nonlinear-optimisation cases, which left referees only about 99% certain of its correctness after four years of review.
To remove that remaining doubt, Hales launched the Flyspeck project in 2003 to formally verify the entire proof using the HOL Light and Isabelle proof assistants. The project, completed with a large international team in 2014 and published in 2017, produced a machine-checked proof with no residual gaps — a landmark for computer-assisted mathematics. Hales was the Andrew Mellon Professor at the University of Pittsburgh until his retirement in May 2025 and has continued to work on formal proof and its application to other geometric optimisation problems.
Workplaces: University of Michigan, University of Pittsburgh
United States