开普勒猜想

1611 年，开普勒提出，密堆积（立方密堆积或六方密堆积，两者的最大密度均为）是可能的最高密度球体堆积，这一论断被称为开普勒猜想。 寻找最密（不一定是周期性的）球体堆积被称为开普勒问题。

巴克敏斯特·富勒（Buckminster Fuller，1975 年）声称拥有一个证明，但那实际上是对面心立方堆积的描述，而不是对其最优性的证明（Sloane 1998）。 W.-Y. Hsiang（Cipra 1991，Hsiang 1992，1993，Cipra 1993）提出了第二个所谓的开普勒猜想证明，但随后被确定为有缺陷的（Conway等人1994，Hales 1994，Sloane 1998）。 J. H. Conway 认为，任何读过 Hsiang 证明的人都不会怀疑其有效性：那是胡说八道。

此后不久，Hales（1997a）发表了一份详细的计划，描述了如何使用与早期尝试显着不同的方法，并广泛使用计算机计算来证明开普勒猜想。 Hales 随后完成了一个完整的证明，该证明发表在一系列总计超过 250 页的论文中（Cipra 1998）。 Hales（2002）发表了对该证明的通俗概述。 该证明广泛依赖于全局优化、线性规划和区间算术理论的方法。 包含组合数学、区间算术和线性规划的计算机代码和数据文件的计算机文件需要超过 3 GB 的存储空间。

Hales 的证明被证实难以验证。 2003 年，据报道，《数学年刊》的出版物将有一份不寻常的编辑注释，指出尽管一个由 12 名审稿人组成的团队花了四年多的时间来验证该证明，并且审稿人有 99% 的把握认为它是正确的，但该论文的部分内容仍然无法检查（Holden 2003，Szpiro 2003）。 然而，实际出版物中没有这样的注释（Hales 2005）。

为了回应验证其证明的困难，2003 年 1 月，Hales 发起了“Flyspeck 项目”（“开普勒的形式证明”），试图使用计算机自动验证证明的每个步骤。 该项目最初由 Hales 认为需要 20 人年的劳动（Holden 2003，Szpiro 2003），于 2014 年完成。