Thomas Callister Hales

Thomas Callister Hales (San Antonio, 4 giugno 1958) è un matematico statunitense attivo nei settori della teoria delle rappresentazioni, della geometria discreta e della verifica formale.

Nella teoria delle rappresentazioni è noto per il suo lavoro sul programma Langlands e per la dimostrazione del lemma fondamentale sul gruppo simplettico Sp(4) (molte delle sue idee furono incorporate nella dimostrazione finale del lemma fondamentale, dovuta a Ngô Bảo Châu). Nella geometria discreta, stabilì la congettura di Keplero sulla densità degli impacchettamenti di sfere e la congettura del nido d'ape. Nel 2014 ha annunciato il completamento del Progetto Flyspeck, che ha verificato formalmente la correttezza della sua dimostrazione della congettura di Keplero.

Ha conseguito il dottorato di ricerca all'Università di Princeton nel 1986 con una tesi dal titolo "The Subregular Germ of Orbital Integrals"^[1]. Successivamente ha insegnato all'Università di Harvard e all'Università di Chicago^[2] e dal 1993 al 2002 ha lavorato presso l'Università del Michigan^[3].

Nel 1998, Hales presentò il suo articolo sulla dimostrazione con assistenza computerizzata della congettura di Keplero, un problema secolare di geometria discreta in cui si afferma che il modo più efficiente in termini di spazio per impacchettare le sfere è a forma di tetraedro. È stato assistito dallo studente laureato Samuel Ferguson^[4]. Nel 1999 Hales dimostrò la congettura del nido d'ape e affermò anche che la congettura potrebbe essere stata nella mente dei matematici prima di Marco Terenzio Varrone.

Dal 2002, Hales divenne professore di matematica dell'Università di Pittsburgh. Nel 2003, Hales iniziò a lavorare su Flyspeck per verificare che la sua dimostrazione della congettura di Keplero fosse corretta. Questa verifica si basava sul calcolo computerizzato e il progetto ha utilizzato due dimostratori di teoremi, HOL Light e Isabelle^[5]. Gli Annals of Mathematics hanno accettato la dimostrazione nel 2005 anche se avevano la sicurezza della prova al 99%^[5]. Nell'agosto 2014, il software del team Flyspeck ha finalmente verificato che la dimostrazione fosse corretta^[5][6].

Nel 2017 Hales ha avviato il progetto Formal Abstracts che mira a fornire dichiarazioni formalizzate dei principali risultati di ciascun articolo di ricerca matematica nel linguaggio di un dimostratore di teoremi interattivo. L'obiettivo di questo progetto è quello di beneficiare della maggiore precisione e interoperabilità fornite dalla formalizzazione informatica, evitando allo stesso tempo lo sforzo che attualmente comporta una formalizzazione su vasta scala di tutte le prove pubblicate. A lungo termine, il progetto spera di costruire un corpus di fatti matematici che consenta l'applicazione di tecniche di apprendimento automatico nella dimostrazione di teoremi interattiva e automatizzata^[7].

Hales ha vinto il Premio Chauvenet nel 2003^[8] e il Paul R. Halmos – Lester R. Ford Award nel 2008^[9]. Nel 2012 è diventato membro dell'American Mathematical Society^[10]. È stato invitato a tenere le Tarski Lectures nel 2019; le sue tre conferenze erano intitolate "Una prova formale della congettura di Keplero", "Formalizzazione della matematica" e "Integrazione con la logica"^[11].

• Thomas C. Hales, The status of the Kepler conjecture, in The Mathematical Intelligencer, vol. 16, n. 3, 1994, pp. 47–58, DOI:10.1007/BF03024356, ISSN 0343-6993 (WC · ACNP), PMID 1281754.
• Thomas C. Hales, The Honeycomb Conjecture, in Discrete and Computational Geometry, vol. 25, n. 1, 2001, pp. 1–22, DOI:10.1007/s004540010071, PMID 1797293.
• Thomas C. Hales, A proof of the Kepler conjecture, in Annals of Mathematics, vol. 162, n. 3, 2005, pp. 1065–1185, DOI:10.4007/annals.2005.162.1065.
• Thomas C. Hales, Historical overview of the Kepler conjecture, in Discrete & Computational Geometry, vol. 36, n. 1, 2006, pp. 5–20, DOI:10.1007/s00454-005-1210-2, ISSN 0179-5376 (WC · ACNP), PMID 2229657.
• Thomas C. Hales e Samuel P. Ferguson, A formulation of the Kepler conjecture, in Discrete & Computational Geometry, vol. 36, n. 1, 2006, pp. 21–69, DOI:10.1007/s00454-005-1211-1, ISSN 0179-5376 (WC · ACNP), PMID 2229658.
• Thomas C. Hales e Samuel P. Ferguson, The Kepler Conjecture: The Hales-Ferguson Proof, New York, Springer, 2011, ISBN 978-1-4614-1128-4.
• Thomas C. Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu e Roland Zumkeller, A formal proof of the Kepler conjecture, in Forum of Mathematics, Pi, vol. 5, 2017, p. e2, DOI:10.1017/fmp.2017.1.

• Wikimedia Commons contiene immagini o altri file su Thomas Callister Hales

Portale Biografie

Portale Matematica