ケプラー予想

3次元ユークリッド空間において、互いに重なり合わない等しい球をどう配置しても、密度が $\pi/\sqrt{18} \approx 0.74048$ を超えることはない。この値は面心立方格子および六方最密充填の密度であり、八百屋がオレンジを、あるいは大砲の弾を積み上げるときの、あの見慣れた積み方である。

ヘイルズは1998年（サミュエル・ファーガソンと共に）、有限個の局所配置への古典的な還元と、約5,000通りの場合について線形計画法の限界を調べる網羅的なコンピュータ探索とを組み合わせた証明を発表した。2003年、12人からなる査読団は、証明が「99%確実」に正しいと報告したが、コンピュータによるすべての計算を手作業で検証することはできなかった。そのため『アナルズ・オブ・マスマティクス』誌はその注記を付けたまま2005年にこの証明を掲載した。その後ヘイルズが率いるフライスペック計画は、証明支援系HOL LightとIsabelleによって一行ずつ検証された完全な形式的証明を構築し、残っていた疑念を取り除いた。フライスペック計画は2014年に完了が発表され、形式的証明は2017年に出版された。