토머스 캘리스터 헤일스

토머스 캘리스터 헤일스(Thomas Callister Hales, 1958년 6월 4일~)는 표현론, 이산기하학, 형식 검증 분야에서 활동하는 미국의 수학자이다. 표현론에서 그는 랭글랜즈 프로그램에 대한 연구와 Sp(4)군에 대한 근본 보조정리의 증명으로 유명하다(그의 아이디어 중 많은 부분이 응오바오쩌우의 근본 보조정리의 최종 증명에 통합되었다). 이산기하학에서는 구 채우기의 밀도에 대한 케플러의 추측, 벌집 추측, 십이면체 추측을 해결했다. 2014년에는 케플러의 추측 증명의 정확성을 형식적으로 검증한 플라이스펙 프로젝트의 완료를 발표했다.

토머스 캘리스터 헤일스
출생	1958년 6월 4일(1958-06-04)(67세) 텍사스주 샌안토니오
국적	미국
교육	프린스턴 대학교 케임브리지 대학교 스탠퍼드 대학교
출신 학교	프린스턴 대학교 케임브리지 대학교 스탠퍼드 대학교
주요 업적	케플러의 추측의 증명 벌집 추측의 증명 십이면체 추측의 증명
수상	쇼브네상 (2003) 무어상 (2004) 데이비드 P. 로빈스 상 (2007) 레스터 R. 포드상 (2008) 풀커슨상 (2009) 타르스키 강연 (2019) 시니어 버윅 상 (2020)
분야	수학
소속	피츠버그 대학교 미시간 대학교 시카고 대학교 하버드 대학교
박사 지도교수	로버트 랭글랜즈
기타 지도교수	로버트 랭글랜즈
박사 지도학생	줄리아 고든
유명한 학생	줄리아 고든

생애

1986년 프린스턴 대학교에서 "궤도 적분의 서브레귤러 싹(The Subregular Germ of Orbital Integrals)"이라는 논문으로 박사 학위를 받았다.^[1][2] 헤일스는 하버드 대학교와 시카고 대학교에서 가르쳤으며,^[3] 1993년부터 2002년까지 미시간 대학교에서 근무했다.^[4]

1998년 컴퓨터를 활용한 증명을 통해 이산기하학에서 수세기 동안 풀리지 않던 문제였던 구를 채우는 가장 공간 효율적인 방법은 사면체 모양이라는 것을 주장한 케플러의 추측을 증명했다. 그는 대학원생 새뮤얼 퍼거슨의 도움을 받았다.^[5] 1999년 헤일스는 벌집 추측을 증명했으며, 이 추측이 마르쿠스 테렌티우스 바로 이전의 수학자들의 마음에 있었을 수도 있다고 언급했다. 이 추측은 알렉산드리아의 파포스가 자신의 책 5권에서 언급했다.

2002년 이후 헤일스는 피츠버그 대학교의 멜런 수학 교수가 되었다. 2003년 헤일스는 케플러 추측 증명을 입증하기 위해 플라이스펙 작업을 시작했다. 증명은 추측을 검증하기 위해 컴퓨터 계산에 의존했다. 이 프로젝트는 두 가지 증명 보조기인 HOL Light와 이자벨을 사용했다.^[6][7][8][9] 수학연보는 2005년에 증명이 99% 확실하다고 확인한다.^[9] 2014년 8월, 플라이스펙 팀의 소프트웨어는 마침내 증명이 정확하다는 것을 검증했다.^[9]

2017년, 수학 연구 논문들의 주요 결과를 대화형 정리 증명기 언어로 형식화된 진술로 제공하는 것을 목표로 하는 형식 초록 프로젝트를 시작했다. 이 프로젝트의 목표는 컴퓨터 형식화가 제공하는 향상된 정밀도와 상호 운용성으로부터 이점을 얻는 동시에 현재 모든 출판된 증명의 완전한 규모의 형식화가 수반하는 노력을 우회하는 것이다. 장기적으로, 이 프로젝트는 대화형 및 자동화된 정리 증명에서 기계 학습 기술의 적용을 허용하는 수학적 사실들의 코퍼스를 구축하기를 희망한다.^[10]

수상 경력

헤일스는 2002년 세계 수학자 대회의 초청 연사였다.^[11] 그는 2003년 쇼브네상을 수상했고,^[12] 2004년 R. E. 무어상을 수상했으며,^[13] 2008년 레스터 R. 포드상을 수상했고,^[14] 2009년 풀커슨상을 수상했다.^[15] 그는 2007년 미국 수학회의 초대 로빈스 상을 수상했다.^[16] 2012년 그는 미국 수학회의 펠로우가 되었다.^[17] 그는 2019년 타르스키 강연에 초청되었다. 그의 세 가지 강연은 "케플러 추측의 형식적 증명", "수학의 형식화", "논리학과의 통합"이었다.^[18][19] 그는 2020년 런던 수학회의 시니어 버윅 상을 수상했다.^[20]

출판물

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