Thomas Callister Hales

From Wikipedia, the free encyclopedia

Thomas Callister Hales
Born {{{birth_date}}}
Residence USA
Nationality American
Field Mathematician
Institution University of Pittsburgh
Alma mater Princeton University
Known for Kepler Conjecture

Thomas Callister Hales is an American mathematician who provided computer-aided proof of the Kepler Conjecture that the most efficient way to pack spheres was in a pyramid shape.

Hales, the 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.


[edit] Education and career

Hales received his Ph.D in mathematics from Princeton University. In 1998, he had a proof of the Kepler Conjecture. Today, he is the University of Pittsburgh Mellon Professor of mathematics.

[edit] References

[edit] External links

In other languages