토머스 캘리스터 헤일스

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

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

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

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

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

수상 경력
헤일스는 2002년 세계 수학자 대회의 초청 연사였다. 그는 2003년 쇼브네상을 수상했고, 2004년 R. E. 무어상을 수상했으며, 2008년 레스터 R. 포드상을 수상했고, 2009년 풀커슨상을 수상했다. 그는 2007년 미국 수학회의 초대 로빈스 상을 수상했다. 2012년 그는 미국 수학회의 펠로우가 되었다.List of Fellows of the American Mathematical Society, retrieved 2013-01-19. 그는 2019년 타르스키 강연에 초청되었다. 그의 세 가지 강연은 "케플러 추측의 형식적 증명", "수학의 형식화", "논리학과의 통합"이었다. 그는 2020년 런던 수학회의 시니어 버윅 상을 수상했다.

출판물

 각주 

 외부 링크 


분류:1958년 출생
분류:살아있는 사람
분류:미시간 대학교 교수
분류:피츠버그 대학교 교수
분류:프린스턴 대학교 동문
분류:샌안토니오 출신
분류:미국 수학회 석학회원
분류:텍사스주의 수학자