Thomas Callister Hales (born June 4, 1958) is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification.

[4] In 1998, Hales submitted his paper on the computer-aided proof of the Kepler conjecture, a centuries-old problem in discrete geometry which states that the most space-efficient way to pack spheres is in a tetrahedron shape.

The conjecture is mentioned by Pappus of Alexandria in his Book V. After 2002, Hales became the University of Pittsburgh's Mellon Professor of Mathematics.

[9] In 2017, he initiated the Formal Abstracts project which aims to provide formalised statements of the main results of each mathematical research paper in the language of an interactive theorem prover.

In the long term, the project hopes to build a corpus of mathematical facts which would allow for the application of machine learning techniques in interactive and automated theorem proving.