开普勒猜想的证明
1998年黑尔斯借助计算机证明球最密堆积密度，2014年形式化验证完成。
背景
开普勒猜想（1611）由约翰内斯·开普勒提出：在三维空间中，相同大小的球最密堆积的密度为
由面心立方堆积（立方密堆积）或六方密堆积达到。这一看似直观的结论，严谨证明却极为困难。
详细描述
1998年，美国数学家托马斯·黑尔斯（Thomas Hales）与其研究生塞缪尔·弗格森（Samuel Ferguson）宣布证明。其思路源自L. Fejes Tóth（1953）：最密堆积问题可归约为在约5000种球构型上验证一组不等式。证明由约250页数学论证与约3GB计算机代码/数据组成，借助线性规划、区间算术与全局优化完成大量组合计算。
《数学年刊》组织12人评审团，4年后表示”99%确信”证明正确，但无法完全验证所依赖的计算机代码。为彻底消除疑虑，黑尔斯于2003年发起 Flyspeck 形式化验证项目，使用证明助手 HOL Light 与 Isabelle，将证明逐步骤机器核验。
求解过程 / 影响（含最新进展若相关）
2014年8月10日，黑尔斯宣布 Flyspeck 项目完成，开普勒猜想的证明首次经过计算机严格形式化验证。这是数学史上又一例（继四色定理之后）依赖、乃至”形式化”计算机的重大证明，展示了形式化方法在核验极其复杂证明中的威力，也推动了”可验证数学”这一方向的发展。值得一提的是，8维与24维球堆积的最密性（由Viazovska等解决，2016）近年亦有突破。