Thomas Callister Hales

Biography

He received his Ph.D. from Princeton University in 1986 with a dissertation titled The Subregular Germ of Orbital Integrals. Hales taught at Harvard University and the University of Chicago, and from 1993 and 2002 he worked at the University of Michigan.

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. He was aided by graduate student Samuel Ferguson. In 1999, Hales proved the honeycomb conjecture, and also stated that the conjecture may have been in the minds of mathematicians before Marcus Terentius Varro. 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. In 2003, Hales started work on Flyspeck to vindicate his proof of the Kepler conjecture. His proof relied on computer calculation to verify conjectures. The project used two proof assistants, HOL Light and Isabelle. Annals of Mathematics accepted the proof in 2005; but was only 99% sure of the proof. In August 2014, the Flyspeck team's software finally verified the proof to be correct.

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. The goal of this project is to benefit from the increased precision and interoperability that computer formalisation provides while circumventing the effort that a full-scale formalisation of all published proofs currently entails. 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.

Hales worked on a conjecture of Karl Reinhardt with Koundinya Vajjha, that the smoothed octagon has the lowest maximum packing density of all centrally symmetric convex shapes in the plane. Although they failed to prove Reinhardt's conjecture, in 2024 they claim to have proved a related conjecture of Kurt Mahler:

Awards

Hales was an invited speaker at the International Congress of Mathematicians in 2002. He won the Chauvenet Prize in 2003, the R. E. Moore Prize in 2004, a Lester R. Ford Award in 2008,{{cite journal

Publications

• {{Cite journal
• {{Cite journal
• {{cite journal
• {{Cite journal
• {{Cite journal
• {{cite journal | article-number=e2

Notes

References

1. "Brief Bio of Thomas C. Hales - thalespitt".
2. Project website https://formalabstracts.github.io/, retrieved 2020-01-10.
3. (2024). "Packings of Smoothed Polygons".
4. "ICM Plenary and Invited Speakers {{!}} International Mathematical Union (IMU)".
5. Hales, Thomas C.. (2000). "Cannonballs and Honeycombs". Notices of the AMS.
6. "Thomas C. Hales Receives Second R. E. Moore Prize".
7. "Browse Prizes and Awards".
8. "Browse Prizes and Awards".
9. [http://www.ams.org/profession/fellows-list List of Fellows of the American Mathematical Society], retrieved 2013-01-19.
10. "2019 Tarski Lectures {{!}} Department of Mathematics at University of California Berkeley".
11. "Group in Logic and the Methodology of Science - Tarski Lectures".
12. "LMS Prize Winners 2020 {{!}} London Mathematical Society".
13. "Thalespitt".
14. [https://github.com/flyspeck/flyspeck Flyspeck Project]
15. "University of Pittsburgh: Department of Mathematics".
16. "Thomas Hales - the Mathematics Genealogy Project".
17. (1992). "The subregular germ of orbital integrals". Memoirs of the American Mathematical Society.
18. "Thomas C. Hales | Faculty History Project".
19. [http://www.umich.edu/~urecord/9899/Sep16_98/hales.htm Hales solves oldest problem in discrete geometry] {{Webarchive. link. (2007-05-29 The University Record (University of Michigan), September 16, 1998)
20. Aron, Jacob. (August 12, 2014). "Proof confirmed of 400-year-old fruit-stacking problem". New Scientist.