开普勒猜想

在三维欧几里得空间中，任何等大且互不重叠的球体排列，其密度都不会超过 $\pi/\sqrt{18} \approx 0.74048$——这正是面心立方堆积和六方最密堆积的密度，也就是水果摊主堆橙子或炮弹时常见的那种堆法。

黑尔斯于1998年（与塞缪尔·弗格森合作）公布了一个证明，将经典的化归为有限多个局部构型，与对约5000种情形进行线性规划界的穷举计算机搜索结合起来。2003年，由十二位审稿人组成的评审团报告称，他们「99%确信」该证明是正确的，但无法逐一手工核验计算机的每一步运算，于是《数学年刊》仍在2005年附带这一说明发表了该证明。此后由黑尔斯领导的Flyspeck项目构建了一个完整的形式化证明，由证明助手HOL Light和Isabelle逐行核验，从而消除了残留的疑虑；Flyspeck项目于2014年宣布完成，其形式化证明于2017年发表。