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.
Biografia
[modifica | modifica wikitesto]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].
Premi e riconoscimenti
[modifica | modifica wikitesto]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].
Pubblicazioni
[modifica | modifica wikitesto]- 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, 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, 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, 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.
Note
[modifica | modifica wikitesto]- ^ (EN) Mathematics Genealogy Project - Thomas Callister Hales, su genealogy.math.ndsu.nodak.edu. URL consultato il 16 gennaio 2024.
- ^ (EN) Brief Bio of Thomas C. Hales - thalespitt, su sites.google.com (archiviato dall'url originale il 27 dicembre 2020).
- ^ (EN) University of Michigan - Faculty History Project, su um2017.org. URL consultato il 16 gennaio 2024 (archiviato dall'url originale il 17 giugno 2018).
- ^ (EN) University of Pittsburgh: Department of Mathematics, su math.pitt.edu (archiviato dall'url originale il 27 settembre 2011).
- ^ a b c (EN) Proof confirmed of 400-year-old fruit-stacking problem, su newscientist.com, New Scientist, 12 agosto 2014. URL consultato il 16 gennaio 2024.
- ^ (EN) Flyspeck Project, su github.com. URL consultato il 16 gennaio 2024.
- ^ (EN) Formal Abstracts Project, su formalabstracts.github.io. URL consultato il 16 gennaio 2024.
- ^ (EN) MAA - Cannonballs and Honeycombs, su maa.org. URL consultato il 16 gennaio 2024.
- ^ (EN) MAA - The Jordan Curve Theorem, Formally and Informally, su maa.org. URL consultato il 16 gennaio 2024.
- ^ (EN) AMS - List of Fellows of the American Mathematical Society, su ams.org. URL consultato il 16 gennaio 2024.
- ^ (EN) Group in Logic and the Methodology of Science - Past events, su logic.berkeley.edu. URL consultato il 16 gennaio 2024.
Altri progetti
[modifica | modifica wikitesto]
Wikimedia Commons contiene immagini o altri file su Thomas Callister Hales
| Controllo di autorità | VIAF (EN) 265904557 · ISNI (EN) 0000 0003 8265 9564 · LCCN (EN) n85251565 · GND (DE) 137005822 · BNF (FR) cb16694033t (data) · J9U (EN, HE) 987007435453105171 |
|---|
