2015年7月22日，美国匹兹堡大学数学系教授Tom Hales应国家数学与交叉科学中心的邀请，做了题为“The Formal Proof of the Kepler Conjecture”的综合报告。报告由交叉中心先进制造部副主任李子明研究员主持，黄飞敏研究员和宗传明教授等出席了会议。

在讲座中，Hales教授介绍了Kepler猜想，和形式验证的方法，讨论了形式验证在数学研究中的应用前景。1611年开普勒猜想：在一个容器中放入等半径的球的平均密度不大于pi/squareroot(18) 。1998年Hales教授宣称他证明了这一著名猜想。他的证明包括数学证明部分和计算机验证部分。数学证明部分于2005年发表于Annals of Mathematics，而计算部分由他和Fuguson在后续文章中给出。2014年8月，Hales和他的合作者形式验证了证明中计算机程序的正确性。

报告人简介：Tom Hales 美国匹兹堡大学数学系Mellon教授。为Langlands计划的基本引理的证明做出了重要贡献，并在计算机的辅助下，证明了Kepler猜想。 获得多项数学奖励，2012年成为AMS Fellow。