stringtranslate.com

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 Langlands y la prueba del lema fundamental sobre el grupo Sp(4) (muchas de sus ideas fueron incorporadas en la prueba final del lema fundamental, debido a Ngô Bảo Châu ). En geometría discreta , resolvió la conjetura de Kepler sobre la densidad de empaquetamientos de esferas y la conjetura del panal . En 2014, anunció la finalización del Proyecto Flyspeck, que verificó formalmente la corrección de su prueba de la conjetura de Kepler .

Biografía

Recibió su doctorado de la Universidad de Princeton en 1986 con una disertación titulada El germen subregular de las integrales orbitales . [2] [3] Hales enseñó en la Universidad de Harvard y la Universidad de Chicago , [4] y entre 1993 y 2002 trabajó en la Universidad de Michigan . [5]

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 términos de espacio para empaquetar esferas es en forma de tetraedro. Fue ayudado por el estudiante de posgrado Samuel Ferguson. [6] En 1999, Hales demostró la conjetura del panal de abejas y también afirmó que la conjetura puede haber estado en las mentes de los matemáticos antes de Marco Terencio Varrón . La conjetura es mencionada por Pappus de Alejandría en su Libro V.

Después de 2002, Hales se convirtió en el Profesor Mellon de Matemáticas de la Universidad de Pittsburgh . En 2003, Hales comenzó a trabajar en Flyspeck para reivindicar su prueba de la conjetura de Kepler. Su prueba se basó en el cálculo informático para verificar las 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 solo estaba 99% seguro de la prueba. [10] En agosto de 2014, el software del equipo Flyspeck finalmente verificó que la prueba era correcta. [10]

En 2017, inició el proyecto Formal Abstracts, cuyo objetivo es proporcionar declaraciones formalizadas de los principales resultados de cada artículo 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 al mismo tiempo 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]

Premios y membresías

Hales ganó el Premio Chauvenet en 2003 [12] y un Premio Lester R. Ford en 2008. [13] En 2012 se convirtió en miembro de la American Mathematical Society . [14] Fue invitado a dar las Tarski Lectures en 2019. Sus tres conferencias se titulaban "Una prueba formal de la conjetura de Kepler", "Formalización de las matemáticas" e "Integración con la lógica". [15] [16]

Publicaciones

Notas

  1. ^ "Thomas Hales | Departamento de Matemáticas | Universidad de Pittsburgh".
  2. ^ "Thomas Hales - El Proyecto de Genealogía Matemática".
  3. ^ Hales, Thomas C. (1992). "El germen subregular de las integrales orbitales" (PDF) . Memorias de la American Mathematical Society . 99 (476). doi :10.1090/MEMO/0476. S2CID  121175826. Archivado desde el original (PDF) el 29 de febrero de 2020.
  4. ^ "Breve biografía de Thomas C. Hales - thalespitt". Archivado desde el original el 27 de diciembre de 2020.
  5. ^ "Copia archivada". Archivado desde el original el 17 de junio de 2018. Consultado el 29 de diciembre de 2016 .{{cite web}}: CS1 maint: copia archivada como título ( enlace )
  6. ^ "Universidad de Pittsburgh: Departamento de Matemáticas". Archivado desde el original el 27 de septiembre de 2011. Consultado el 29 de diciembre de 2016 .
  7. ^ "Talespitt".
  8. ^ Proyecto Flyspeck
  9. ^ Hales resuelve el problema más antiguo de la geometría discreta Archivado el 29 de mayo de 2007 en Wayback Machine. The University Record (Universidad de Michigan), 16 de septiembre de 1998
  10. ^ abc Aron, Jacob (12 de agosto de 2014). «Prueba confirmada de un problema de apilamiento de frutas de hace 400 años». New Scientist . Consultado el 10 de mayo de 2017 .
  11. ^ Sitio web del proyecto https://formalabstracts.github.io/, consultado el 10 de enero de 2020.
  12. ^ Hales, Thomas C. (2000). "Balas de cañón y panales". Avisos de la AMS . 47 (4): 440–449.
  13. ^ Hales, Thomas C. (2007). "El teorema de la curva de Jordan, formal e informalmente". American Mathematical Monthly . 114 (10): 882–894. doi :10.1080/00029890.2007.11920481. JSTOR  27642361. S2CID  887392.
  14. ^ Lista de miembros de la American Mathematical Society, consultado el 19 de enero de 2013.
  15. ^ "Conferencias Tarski 2019 | Departamento de Matemáticas de la Universidad de California en Berkeley". math.berkeley.edu . Consultado el 2 de noviembre de 2021 .
  16. ^ "Grupo de Lógica y Metodología de la Ciencia - Conferencias Tarski". logic.berkeley.edu . Consultado el 2 de noviembre de 2021 .

Enlaces externos