トーマス・ヘイルズ
活動期 1958年頃, アメリカ合衆国テキサス州サンアントニオ
1998年に球充填に関するケプラー予想を証明し、その後証明を完全に形式化・コンピュータ検証するフライスペックプロジェクトを主導したアメリカの数学者。
トーマス・ヘイルズはテキサス州サンアントニオで生まれ、スタンフォード大学とケンブリッジで学び、1986年にプリンストン大学でロバート・ラングランズの指導のもとラングランズ・プログラムの研究で博士号を取得した。ハーバード大学、シカゴ大学、高等研究所で教えた後、1993年にミシガン大学に着任した。
1998年、ラースロー・フェイェシュ・トートが1953年に提案した戦略を土台に、ヘイルズは大学院生サミュエル・ファーガソンとともにケプラー予想——面心立方格子と六方最密充填が空間における等球の最密充填を実現するという、ケプラーが1611年に主張した命題——を証明した。この証明は古典解析と約300ページの論証、そして問題を数千の非線形最適化の場合に帰着させるギガバイト規模のコンピュータ計算を組み合わせたもので、4年間の査読を経ても正しさについて約99%の確信しか得られなかった。
この残る疑念を取り除くため、ヘイルズは2003年にフライスペックプロジェクトを立ち上げ、HOL LightとIsabelleという証明支援系を用いて証明全体を形式的に検証した。大規模な国際チームとともに2014年に完了し2017年に発表されたこのプロジェクトは、残存する欠陥のない機械検証済み証明を生み出し、コンピュータ支援数学における画期的な成果となった。ヘイルズは2025年5月に退職するまでピッツバーグ大学のアンドリュー・メロン教授を務め、現在も形式証明とその他の幾何学的最適化問題への応用研究を続けている。
所属先: ミシガン大学, ピッツバーグ大学
アメリカ合衆国