# Thomas Callister Hales : biography

**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.

## Notes

## Education

He received his Ph.D. from Princeton University.

## 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. at the University of Pittsburgh Math Department The University Record (University of Michigan), September 16, 1998

In 2012 he became a fellow of the American Mathematical Society., retrieved 2013-01-19.