开普勒猜想
相同球体最密堆积密度为 π/√18；1611 年开普勒提出，1998 年黑尔斯证明。
详细描述
1611 年，天文学家约翰内斯·开普勒（Johannes Kepler）在论述雪花六角形的小册子中提出：在三维空间中，用全等同大球体做最密堆积时，所能达到的最大平均密度，由超市里常见的”面心立方”（逐层密铺，每层六边形排列）实现，其密度为 。换言之，任何非重叠的等球堆积，其密度都不超过这一值。这就是开普勒猜想（Kepler conjecture），是离散几何与球堆积理论的源头问题。
求解过程
- 费耶什·托特（L. Fejes Tóth, 1953） 指出，该问题可化为在有限多个变量上极小化一个函数，为计算机证明指明方向。
- 托马斯·黑尔斯（Thomas Hales, 1998） 与研究生塞缪尔·弗格森（Samuel Ferguson）把问题归约为约 5000 种构型的线性规划验证，用约 250 页数学论证加数千页计算机代码，于 1998 年 8 月宣布证明。2005 年《数学年刊》接受，但审稿人仅表示”99% 确信”，因无法核查全部代码。
- 为消除疑虑，黑尔斯于 2003 年发起 Flyspeck 形式化验证工程，用 HOL Light 与 Isabelle 两个证明助手逐项机器核验。2014 年 8 月，他宣布工程完成，开普勒猜想由此成为首个经完全形式化验证的重大定理。
意义
开普勒猜想把”怎样堆得最密”这一朴素问题，变成了连接几何、优化与计算证明的枢纽。Flyspeck 的成功展示了用计算机对数百页证明做端到端形式化验证的可行性，为可信的机器辅助数学树立了标杆。