Thomas Callister Hales | ||
---|---|---|
![]() | ||
Información personal | ||
Nacimiento |
4 de junio de 1958 San Antonio (Estados Unidos) | (66 años)|
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 | Sociedad Estadounidense de Matemática (desde 2012) | |
Distinciones |
| |
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.
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]
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]