Thomas Callister Hales - Thomas Callister Hales
Thomas Hales | |
---|---|
![]() | |
narozený | |
Národnost | americký |
Alma mater | Univerzita Princeton |
Známý jako | Prokazující Keplerova domněnka |
Ocenění |
|
Vědecká kariéra | |
Pole | Matematika |
Instituce | University of Pittsburgh[1] Michiganská univerzita |
Doktorský poradce | Robert Langlands |
Doktorandi | Julia Gordon |
webová stránka | stránky |
Thomas Callister Hales (narozen 4. června 1958) je americký matematik pracující v oblastech teorie reprezentace, diskrétní geometrie, a formální ověření. v teorie reprezentace on je známý pro jeho práci na Langlandsův program a důkaz o základní lemma přes skupinu Sp (4) (mnoho z jeho nápadů bylo zapracováno do konečného důkazu kvůli Ngô Bảo Châu ). v diskrétní geometrie, usadil se Keplerova domněnka na hustotu koule balení a plástová domněnka. V roce 2014 oznámil dokončení projektu Flyspeck, který formálně ověřil správnost jeho důkazu o Keplerova domněnka.
Životopis
Získal titul Ph.D. z Univerzita Princeton v roce 1986 byla jeho disertační práce pojmenována Subregulární zárodek orbitálních integrálů.[2][3] V letech 1993 až 2002 pracoval v Michiganská univerzita.[4]
V roce 1998 Hales předložil svůj příspěvek o počítači důkaz z Keplerova domněnka; staletý problém v diskrétní geometrie což uvádí, že vesmírně nejefektivnější způsob zabalit koule je ve tvaru čtyřstěnu. Pomohl mu postgraduální student Samuel Ferguson.[5] V roce 1999 Hales prokázal plástová domněnka, také uvedl, že domněnka mohla existovat v myslích matematiků již dříve Marcus Terentius Varro.
Po roce 2002 se Hales stal University of Pittsburgh Mellon je profesorem matematiky. V roce 2003 začal Hales pracovat na společnosti Flyspeck, aby obhájil svůj důkaz o Keplerově domněnce. Jeho důkaz se spoléhal na počítačový výpočet k ověření domněnek. V projektu byly použity dva důkazní asistenti; HOL Light a Isabelle.[6][7][8][9] Annals of Mathematics důkaz přijal v roce 2005; ale důkazem si byl jistý pouze na 99%.[9] V srpnu 2014 software týmu Flyspeck konečně ověřil, zda je důkaz správný.[9]
V roce 2017 zahájil projekt Formální abstrakty, jehož cílem je poskytnout formalizovaná prohlášení o hlavních výsledcích každé matematické výzkumné práce v jazyce interaktivní věta prover. Cílem tohoto projektu je těžit ze zvýšené přesnosti a interoperability, kterou poskytuje počítačová formalizace, a zároveň obejít úsilí, které v současné době přináší formalizace všech publikovaných důkazů v plném rozsahu. V dlouhodobém horizontu projekt doufá, že vytvoří korpus matematických faktů, který by umožnil použití technik strojového učení v interaktivním a automatizovaném dokazování teorémů.[10]
Ocenění a členství
Hales vyhrál Cena Chauvenet v roce 2003[11] a a Cena Lestera R. Forda v roce 2008.[12] V roce 2012 se stal členem Americká matematická společnost.[13]
Publikace
- Hales, Thomas C. (1994), „Stav Keplerova domněnky“, Matematický zpravodaj, 16 (3): 47–58, doi:10.1007 / BF03024356, ISSN 0343-6993, PAN 1281754
- Hales, Thomas C. (2001). „Voštinová domněnka“. Diskrétní a výpočetní geometrie. 25 (1): 1–22. arXiv:matematika / 9906042. doi:10.1007 / s004540010071. PAN 1797293.
- Hales, Thomas C. (2005). "Důkaz o Keplerově domněnce". Annals of Mathematics. 162 (3): 1065–1185. arXiv:matematika / 9811078. doi:10.4007 / annals.2005.162.1065.
- Hales, Thomas C. (2006), „Historický přehled Keplerova domněnky“, Diskrétní a výpočetní geometrie, 36 (1): 5–20, doi:10.1007 / s00454-005-1210-2, ISSN 0179-5376, PAN 2229657
- Hales, Thomas C .; Ferguson, Samuel P. (2006), „Formulace Keplerova domněnky“, Diskrétní a výpočetní geometrie, 36 (1): 21–69, arXiv:matematika / 9811078, doi:10.1007 / s00454-005-1211-1, ISSN 0179-5376, PAN 2229658
- Hales, Thomas C .; Ferguson, Samuel P. (2011), Keplerova domněnka: Hales-Fergusonův důkaz, New York: Springer, ISBN 978-1-4614-1128-4
- Hales, Thomas C .; Adams, Mark; Bauer, Gertrud; Dat Tat Dang; Harrison, John; Truong Le Hoang; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Thang Tat Nguyen; Truong Quang Nguyen; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jasone; Solovjev, Alexej; Hoai Thi Ta; Trung Nam Tran; Diep Thi Trieu; Urban, Josef; Ky Khac Vu; Zumkeller, Roland (2015). „Formální důkaz Keplerova domněnky“. arXiv:1501.02155 [math.MG ].
Poznámky
- ^ http://www.mathematics.pitt.edu/person/thomas-hales
- ^ https://www.genealogy.math.ndsu.nodak.edu/id.php?id=77593
- ^ https://pdfs.semanticscholar.org/d773/09af42214089a8a416a2423c4c0add8c97ac.pdf
- ^ http://um2017.org/faculty-history/faculty/thomas-c-hales
- ^ http://www.math.pitt.edu/articles/cannonOverview.html
- ^ https://sites.google.com/site/thalespitt/
- ^ Flyspeck Project
- ^ Hales řeší nejstarší problém v diskrétní geometrii The University Record (University of Michigan), 16. září 1998
- ^ A b C Aron, Jacob (12. srpna 2014). „Důkaz potvrzuje 400 let starý problém se stohováním ovoce“. Nový vědec. Citováno 10. května 2017.
- ^ Web projektu https://formalabstracts.github.io/, vyvoláno 2020-01-10.
- ^ Hales, Thomas C. (2000). „Dělové koule a voštiny“. Oznámení AMS. 47 (4): 440–449.
- ^ Hales, Thomas C. (2007). „Věta Jordanovy křivky, formálně a neformálně“. Amer. Matematika. Měsíční. 114: 882–894. JSTOR 27642361.
- ^ Seznam členů Americké matematické společnosti, vyvoláno 2013-01-19.