Thomas Callister Hales
# 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
## Semblanza

Obtuvo su doctorado por la Universidad de Princeton en 1986. Su tesis se tituló El germen subregular de las integrales orbitales. Hales enseñó en la Universidad de Harvard y en la Universidad de Chicago, y entre 1993 y 2002 trabajó en la Universidad de Míchigan.
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. 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. 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. Annals of Mathematics aceptó la prueba en 2005; pero con un umbral de seguridad del 99%. En agosto de 2014, el software del equipo de Flyspeck finalmente verificó que la demostración era correcta.
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.

# Thomas Callister Hales
## Reconocimientos

Hales Ganó el Premio Chauvenet en 2003 y el Premio Lester R. Ford en 2008. En 2012 se convirtió en miembro de la Sociedad Matemática Estadounidense.

# Thomas Callister Hales
## 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. Se sugiere usar |número-autores= (ayuda)