Jump to content

Thomas Callister Hales

From Wikipedia, the free encyclopedia
Thomas Hales
Born (1958-06-04) June 4, 1958 (age 66)
San Antonio, Texas
NationalityAmerican
Alma materPrinceton University
University of Cambridge
Stanford University
Known forProof of the Kepler conjecture
Proof of the honeycomb conjecture
Proof of the dodecahedral conjecture
Awards
Scientific career
FieldsMathematics
InstitutionsUniversity of Pittsburgh
University of Michigan
University of Chicago
Harvard University
Doctoral advisorRobert Langlands
Doctoral studentsJulia Gordon
Websitesites.google.com/site/thalespitt/

Thomas Callister Hales (born June 4, 1958) is an American mathematician working in the areas of representation theory, discrete geometry, and formal verification. In representation theory he is known for his work on the Langlands program and the proof of the fundamental lemma over the group Sp(4) (many of his ideas were incorporated into the final proof of the fundamental lemma, due to Ngô Bảo Châu). In discrete geometry, he settled the Kepler conjecture on the density of sphere packings, the honeycomb conjecture, and the dodecahedral conjecture. In 2014, he announced the completion of the Flyspeck Project, which formally verified the correctness of his proof of the Kepler conjecture.

Biography

[edit]

He received his Ph.D. from Princeton University in 1986 with a dissertation titled The Subregular Germ of Orbital Integrals.[1][2] Hales taught at Harvard University and the University of Chicago,[3] and from 1993 and 2002 he worked at the University of Michigan.[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. He was aided by graduate student Samuel Ferguson.[5] 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.[6][7][8][9] Annals of Mathematics accepted the proof in 2005; but was only 99% sure of the proof.[9] In August 2014, the Flyspeck team's software finally verified the proof to be correct.[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. 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.[10]

Awards

[edit]

Hales was an invited speaker at the International Congress of Mathematicians in 2002.[11] He won the Chauvenet Prize in 2003,[12] the R. E. Moore Prize in 2004,[13] a Lester R. Ford Award in 2008,[14] and a Fulkerson Prize in 2009.[15] He was awarded the inaugural Robbins Prize of the American Mathematical Society in 2007.[16] In 2012 he became a fellow of the American Mathematical Society.[17] He was invited to give the Tarski Lectures in 2019. His three lectures were titled "A formal proof of the Kepler conjecture", "Formalizing mathematics", and "Integrating with Logic".[18][19] He was awarded the Senior Berwick Prize of the London Mathematical Society in 2020.[20]

Publications

[edit]
  • Hales, Thomas C. (1994). "The status of the Kepler conjecture". The Mathematical Intelligencer. 16 (3): 47–58. doi:10.1007/BF03024356. ISSN 0343-6993. MR 1281754. S2CID 123375854.
  • Hales, Thomas C. (2001). "The Honeycomb Conjecture". Discrete and Computational Geometry. 25 (1): 1–22. arXiv:math/9906042. doi:10.1007/s004540010071. MR 1797293. S2CID 14849112.
  • Hales, Thomas C. (2005). "A proof of the Kepler conjecture". Annals of Mathematics. 162 (3): 1065–1185. arXiv:math/9811078. doi:10.4007/annals.2005.162.1065.
  • Hales, Thomas C. (2006). "Historical overview of the Kepler conjecture". Discrete & Computational Geometry. 36 (1): 5–20. doi:10.1007/s00454-005-1210-2. ISSN 0179-5376. MR 2229657.
  • Hales, Thomas C.; Ferguson, Samuel P. (2006). "A formulation of the Kepler conjecture". Discrete & Computational Geometry. 36 (1): 21–69. arXiv:math/9811078. doi:10.1007/s00454-005-1211-1. ISSN 0179-5376. MR 2229658. S2CID 6529590.
  • Hales, Thomas C.; Ferguson, Samuel P. (2011), The Kepler Conjecture: The Hales-Ferguson Proof, New York: Springer, ISBN 978-1-4614-1128-4
  • Hales, Thomas C.; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Truong Le; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; An Hoai Thi Ta; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland (2017). "A formal proof of the Kepler conjecture". Forum of Mathematics, Pi. 5: e2. arXiv:1501.02155. doi:10.1017/fmp.2017.1.

Notes

[edit]
  1. ^ "Thomas Hales - the Mathematics Genealogy Project".
  2. ^ Hales, Thomas C. (1992). "The subregular germ of orbital integrals" (PDF). Memoirs of the American Mathematical Society. 99 (476). doi:10.1090/MEMO/0476. S2CID 121175826. Archived from the original (PDF) on 2020-02-29.
  3. ^ "Brief Bio of Thomas C. Hales - thalespitt". Archived from the original on 2020-12-27.
  4. ^ "Archived copy". Archived from the original on 2018-06-17. Retrieved 2016-12-29.{{cite web}}: CS1 maint: archived copy as title (link)
  5. ^ "University of Pittsburgh: Department of Mathematics". Archived from the original on 2011-09-27. Retrieved 2016-12-29.
  6. ^ "Thalespitt".
  7. ^ Flyspeck Project
  8. ^ Hales solves oldest problem in discrete geometry Archived 2007-05-29 at the Wayback Machine The University Record (University of Michigan), September 16, 1998
  9. ^ a b c Aron, Jacob (August 12, 2014). "Proof confirmed of 400-year-old fruit-stacking problem". New Scientist. Retrieved May 10, 2017.
  10. ^ Project website https://formalabstracts.github.io/, retrieved 2020-01-10.
  11. ^ "ICM Plenary and Invited Speakers | International Mathematical Union (IMU)". www.mathunion.org. Retrieved 2024-10-13.
  12. ^ Hales, Thomas C. (2000). "Cannonballs and Honeycombs". Notices of the AMS. 47 (4): 440–449.
  13. ^ "Thomas C. Hales Receives Second R. E. Moore Prize". www.reliable-computing.org. Retrieved 2024-10-13.
  14. ^ Hales, Thomas C. (2007). "The Jordan Curve Theorem, Formally and Informally". American Mathematical Monthly. 114 (10): 882–894. doi:10.1080/00029890.2007.11920481. JSTOR 27642361. S2CID 887392.
  15. ^ "Browse Prizes and Awards". American Mathematical Society. Retrieved 2024-10-13.
  16. ^ "Browse Prizes and Awards". American Mathematical Society. Retrieved 2024-10-13.
  17. ^ List of Fellows of the American Mathematical Society, retrieved 2013-01-19.
  18. ^ "2019 Tarski Lectures | Department of Mathematics at University of California Berkeley". math.berkeley.edu. Retrieved 2021-11-02.
  19. ^ "Group in Logic and the Methodology of Science - Tarski Lectures". logic.berkeley.edu. Retrieved 2021-11-02.
  20. ^ "LMS Prize Winners 2020 | London Mathematical Society". www.lms.ac.uk. Retrieved 2024-10-13.
[edit]
Retrieved from "https://en.wikipedia.org/w/index.php?title=Thomas_Callister_Hales&oldid=1251063340"