Thomas Callister Hales - Thomas Callister Hales
Thomas Hales | |
|---|---|
 | |
| Nació |
4 de junio de 1958 |
| Nacionalidad | americano |
| alma mater | Universidad de Princeton |
| Conocido por | Demostrar la conjetura de Kepler |
| Premios | |
| Carrera científica | |
| Los campos | Matemáticas |
| Instituciones |
Universidad de Pittsburgh Universidad de Michigan |
| Asesor de doctorado | Robert Langlands |
| Estudiantes de doctorado | Julia Gordon |
| Sitio web | sitios |
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 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 de los empaques de esferas y la conjetura del panal . En 2014, anunció la finalización del Proyecto Flyspeck, que verificó formalmente la exactitud de su prueba de la conjetura de Kepler .
Biografía
Recibió su Ph.D. de 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 la Universidad de Chicago , y desde 1993 y 2002 trabajó en la Universidad de Michigan .
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 cuanto al espacio para empaquetar esferas es en forma de tetraedro. Fue ayudado por el estudiante graduado Samuel Ferguson. En 1999, Hales probó la conjetura del panal , también afirmó que la conjetura pudo haber estado presente en las mentes de los matemáticos antes de Marcus Terentius Varro .
Después de 2002, Hales se convirtió en profesor de matemáticas Mellon de la Universidad de Pittsburgh . En 2003, Hales 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 estaba solo 99% seguro de la prueba. En agosto de 2014, el software del equipo Flyspeck finalmente verificó que la prueba 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.
Premios y membresías
Hales ganó el premio Chauvenet en 2003 y un premio Lester R. Ford en 2008. En 2012 se convirtió en miembro de la American Mathematical Society .
Publicaciones
- Hales, Thomas C. (1994). "El estado de la conjetura de Kepler" . El inteligente matemático . 16 (3): 47–58. doi : 10.1007 / BF03024356 . ISSN 0343-6993 . Señor 1281754 . S2CID 123375854 .
- Hales, Thomas C. (2001). "La conjetura del panal" . Geometría discreta y computacional . 25 (1): 1–22. arXiv : matemáticas / 9906042 . doi : 10.1007 / s004540010071 . Señor 1797293 . S2CID 14849112 .
- Hales, Thomas C. (2005). "Una prueba de la conjetura de Kepler" . Annals of Mathematics . 162 (3): 1065-1185. arXiv : matemáticas / 9811078 . doi : 10.4007 / annals.2005.162.1065 .
- Hales, Thomas C. (2006). "Reseña histórica de la conjetura de Kepler" . Geometría discreta y computacional . 36 (1): 5-20. doi : 10.1007 / s00454-005-1210-2 . ISSN 0179-5376 . Señor 2229657 .
- Hales, Thomas C .; Ferguson, Samuel P. (2006). "Una formulación de la conjetura de Kepler" . Geometría discreta y computacional . 36 (1): 21–69. arXiv : matemáticas / 9811078 . doi : 10.1007 / s00454-005-1211-1 . ISSN 0179-5376 . Señor 2229658 . S2CID 6529590 .
- Hales, Thomas C .; Ferguson, Samuel P. (2011), La conjetura de Kepler: La prueba de Hales-Ferguson , Nueva 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, Víctor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobías; 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). "Una prueba formal de la conjetura de Kepler" . Foro de Matemáticas, Pi . 5 : e2. arXiv : 1501.02155 . doi : 10.1017 / fmp.2017.1 .