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, gracias a Ngô Bảo Châu ). En geometría discreta , resolvió la conjetura de Kepler sobre la densidad de los empaquetamientos esféricos 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 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 en la Universidad de Chicago , [4] y desde 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 centenario en geometría discreta que establece que la forma más eficiente desde el punto de vista espacial para empaquetar esferas es en forma de tetraedro. Fue ayudado por el estudiante graduado Samuel Ferguson. [6] En 1999, Hales demostró la conjetura del panal y también afirmó que la conjetura puede haber estado en la mente de los matemáticos anteriores a Marco Terencio Varro .

Después de 2002, Hales se convirtió en profesor Mellon de Matemáticas de la Universidad de Pittsburgh . En 2003, Hales empezó a trabajar en Flyspeck para reivindicar su prueba de la conjetura de Kepler. Su prueba se basó en cálculos informáticos 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 sólo estaba 99% seguro de la prueba. [10] En agosto de 2014, el software del equipo de 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 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 y al mismo tiempo evitar el esfuerzo que implica 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 permitiría la aplicación de técnicas de aprendizaje automático en la demostración de teoremas interactiva y automatizada. [11]

Premios y membresías

Hales ganó el Premio Chauvenet en 2003 [12] y el Premio Lester R. Ford en 2008. [13] En 2012 se convirtió en miembro de la Sociedad Estadounidense de Matemáticas . [14] Fue invitado a dar las Conferencias Tarski en 2019. Sus tres conferencias se titularon "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 de las matemáticas".
  3. ^ Hales, Thomas C. (1992). «El germen subregular de las integrales orbitales» (PDF) . Memorias de la Sociedad Matemática Estadounidense . 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}}: Mantenimiento CS1: 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. ^ "Thalespitt".
  8. ^ Proyecto Flyspeck
  9. ^ Hales resuelve el problema más antiguo en 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". Científico nuevo . 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". Mensual Matemático Estadounidense . 114 (10): 882–894. doi :10.1080/00029890.2007.11920481. JSTOR  27642361. S2CID  887392.
  14. ^ Lista de miembros de la Sociedad Estadounidense de Matemáticas, consultado el 19 de enero de 2013.
  15. ^ "Conferencias Tarski 2019 | Departamento de Matemáticas de la Universidad de California Berkeley". math.berkeley.edu . Consultado el 2 de noviembre de 2021 .
  16. ^ "Grupo de Lógica y Metodología de la Ciencia - Conferencias Tarski". lógica.berkeley.edu . Consultado el 2 de noviembre de 2021 .

enlaces externos