Thomas Callister Hales
June 4, 1958 |
San Antonio, Texas
|Institutions||University of Pittsburgh
University of Michigan
|Alma mater||Princeton University|
|Doctoral advisor||Robert Langlands|
|Known for||Proving Kepler conjecture|
Thomas Callister Hales (born June 4, 1958) is an American mathematician working on the Langlands program. He is known in the area for having worked on the fundamental lemma, and proving a special case of it over the group Sp(4). Many of his ideas were incorporated into the final proof, due to Ngô Bảo Châu. He is also known for his 1998 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 pyramid shape. Hales also proved the honeycomb conjecture.
Career in mathematics
Hales, formerly at the University of Michigan, and now University of Pittsburgh Mellon Professor of mathematics, advocates the formalization of mathematics to ensure rigor in an era where proofs are becoming increasingly complex and computers are becoming necessary to perform verification. Hales's current project, called Flyspeck, seeks to formalize his proof of the Kepler conjecture in the computer theorem prover HOL Light.   
- Hales's page at the University of Pittsburgh Math Department
- Flyspeck Project
- Hales solves oldest problem in discrete geometry The University Record (University of Michigan), September 16, 1998
- List of Fellows of the American Mathematical Society, retrieved 2013-01-19.