托马斯·黑尔斯
活跃于约1958年, 美国德克萨斯州圣安东尼奥
几何学
美国数学家,1998年证明了关于球体堆积的开普勒猜想,后来主持了Flyspeck项目,给出该证明的完整形式化计算机验证。
托马斯·黑尔斯生于德克萨斯州圣安东尼奥,先后就读于斯坦福大学与剑桥大学,1986年在普林斯顿大学于罗伯特·朗兰兹指导下以朗兰兹纲领研究获得博士学位。他曾在哈佛大学、芝加哥大学和高等研究院任教,1993年加入密歇根大学。
1998年,黑尔斯在拉斯洛·费耶什·托特1953年提出的策略基础上,与研究生塞缪尔·弗格森一起证明了开普勒猜想:面心立方与六方最密堆积在空间中实现了等球的最密堆积,这是开普勒于1611年提出的论断。该证明结合了经典分析、约300页的论证,以及将问题归约为数千个非线性优化情形的数吉字节计算机计算,以至于历经四年审稿后,评审者也只有约99%的把握确信其正确性。
为消除这残留的疑虑,黑尔斯于2003年发起Flyspeck项目,用HOL Light和Isabelle证明助手对整个证明进行形式化验证。该项目由一个庞大的国际团队于2014年完成、2017年发表,产出了没有残余漏洞的机器验证证明——这是计算机辅助数学的一个里程碑。黑尔斯在2025年5月退休前担任匹兹堡大学安德鲁·梅隆教授,目前仍继续从事形式化证明及其在其他几何优化问题中的应用研究。
工作单位: 密歇根大学, 匹兹堡大学
美国