Thomas Callister Hales
Thomas Callister Hales (nacido el 4 de junio de 1958) es un matemático estadounidense que trabaja en las áreas de teoría de la representación, geometría discreta y verificación formal. En teoría de la representación es conocido por su trabajo en el programa de Langlands y la prueba del lema fundamental sobre el grupo Sp(4) (muchas de sus ideas fueron incorporadas a la prueba final, debido a Ngô Bảo Châu). En geometría discreta, estableció la conjetura de Kepler sobre la densidad del empaquetamiento de esferas y la conjetura del panal de abeja. En 2014, anunció la finalización del Proyecto Flyspeck, que verificó formalmente la exactitud de su prueba de la conjetura de Kepler.
| Thomas Callister Hales | ||
|---|---|---|
| Información personal | ||
| Nacimiento | 4 de junio de 1958 (65 años) San Antonio (Estados Unidos) | |
| Nacionalidad | Estadounidense | |
| Educación | ||
| Educado en | Universidad de Princeton | |
| Supervisor doctoral | Robert Langlands | |
| Información profesional | ||
| Ocupación | Matemático y profesor universitario | |
| Área | Matemáticas | |
| Empleador | ||
| Miembro de | American Mathematical Society (desde 2012) | |
| Distinciones |
| |
Semblanza
Obtuvo su doctorado por la Universidad de Princeton en 1986. Su tesis se tituló El germen subregular de las integrales orbitales.[1][2] Hales enseñó en la Universidad de Harvard y en la Universidad de Chicago,[3] y entre 1993 y 2002 trabajó en la Universidad de Míchigan.[4]
En 1998, Hales presentó su artículo sobre la prueba asistida por computadora de la conjetura de Kepler; un problema de siglos de antigüedad en geometría discreta que establece que la forma más eficiente en el espacio de empaquetar esferas es en forma de tetraedro. Fue ayudado por el estudiante graduado Samuel Ferguson.[5] En 1999, Hales probó la conjetura del panal, afirmando que la conjetura pudo haber estado presente en las mentes de los matemáticos antes de Marcus Terentius Varro.
Después de 2002, se convirtió en profesor de matemáticas Mellon de la Universidad de Pittsburgh.[6] En 2003 comenzó a trabajar en Flyspeck para reivindicar su demostración de la conjetura de Kepler. Su prueba se basó en cálculos por computadora para verificar conjeturas. El proyecto utilizó dos asistentes de prueba; HOL Light e Isabelle.[7][8][9][10] Annals of Mathematics aceptó la prueba en 2005; pero con un umbral de seguridad del 99%.[10] En agosto de 2014, el software del equipo de Flyspeck finalmente verificó que la demostración era correcta.[10]
En 2017, inició el proyecto Formal Abstracts que tiene como objetivo proporcionar declaraciones formalizadas de los principales resultados de cada trabajo de investigación matemática en el lenguaje de un demostrador de teoremas interactivo. El objetivo de este proyecto es beneficiarse de la mayor precisión e interoperabilidad que proporciona la formalización informática, evitando el esfuerzo que supone actualmente una formalización a gran escala de todas las pruebas publicadas. A largo plazo, el proyecto espera construir un corpus de hechos matemáticos que permita la aplicación de técnicas de aprendizaje automático en la demostración interactiva y automatizada de teoremas.[11]
Reconocimientos
Hales Ganó el Premio Chauvenet en 2003 y el Premio Lester R. Ford en 2008.[12][13] En 2012 se convirtió en miembro de la Sociedad Matemática Estadounidense.[14]
Publicaciones
- Hales, Thomas C. (1994). «The status of the Kepler conjecture». The Mathematical Intelligencer 16 (3): 47-58. ISSN 0343-6993. doi:10.1007/BF03024356.
- Hales, Thomas C. (2001). «The Honeycomb Conjecture». Discrete and Computational Geometry 25 (1): 1-22. arXiv:math/9906042. doi:10.1007/s004540010071.
- 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. ISSN 0179-5376. doi:10.1007/s00454-005-1210-2.
- Hales, Thomas C.; Ferguson, Samuel P. (2006). «A formulation of the Kepler conjecture». Discrete & Computational Geometry 36 (1): 21-69. ISSN 0179-5376. arXiv:math/9811078. doi:10.1007/s00454-005-1211-1.
- 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 et al. (2017). «A formal proof of the Kepler conjecture». Forum of Mathematics, Pi 5: e2. arXiv:1501.02155. doi:10.1017/fmp.2017.1.
Referencias
- https://www.genealogy.math.ndsu.nodak.edu/id.php?id=77593
- Hales, Thomas C. (1992). . Memoirs of the American Mathematical Society 99 (476). S2CID 121175826. doi:10.1090/MEMO/0476. Archivado desde el original el 29 de febrero de 2020.
- . Archivado desde el original el 17 de junio de 2018. Consultado el 20 de mayo de 2021.
- . Archivado desde el original el 27 de septiembre de 2011. Consultado el 20 de mayo de 2021.
- http://www.mathematics.pitt.edu/person/thomas-hales
- https://sites.google.com/site/thalespitt/
- Flyspeck Project
- Hales solves oldest problem in discrete geometry el 29 de mayo de 2007 en Wayback Machine. The University Record (University of Michigan), September 16, 1998
- ↑ Aron, Jacob (12 de agosto de 2014). «Proof confirmed of 400-year-old fruit-stacking problem». New Scientist. Consultado el 10 de mayo de 2017.
- Project website https://formalabstracts.github.io/, retrieved 2020-01-10.
- Hales, Thomas C. (2000). «Cannonballs and Honeycombs». Notices of the AMS 47 (4): 440-449.
- Hales, Thomas C. (2007). «The Jordan Curve Theorem, Formally and Informally». American Mathematical Monthly 114 (10): 882-894. doi:10.1080/00029890.2007.11920481.
- List of Fellows of the American Mathematical Society, retrieved 2013-01-19.
Enlaces externos
- Thomas Callister Hales en el Mathematics Genealogy Project.