ケプラー予想
等しい大きさの球による球充填から作られるボロノイ多面体の体積は、内接円半径が1である正十二面体の体積より小さくなることがない。
ケプラー予想と関連する問題で、ヘイルズと同様の手法で証明された。マクローリンによる証明は1999年のモーガン賞を受賞した。ラースロー・フェイェシュ=トートが1950年に提示していた予想である。
2003年1月、ヘイルズはケプラー予想の完全な形式的証明を求める共同プロジェクトを開始した。その目標は、証明の妥当性に一切の疑問を残さないため、HOL LightやIsabelleなどの自動証明検証(英語版)プログラムにかけられるような形式的証明を構築することであった。プロジェクトは「Flyspeck」と名付けられた。そのうちの3文字、F、P、Kは「Formal Proof of Kepler」(ケプラーの形式的証明)から取ったものである。ヘイルズは完全な形式的証明を構築するのには20年ほどの作業が必要だと見積もっていた。2014年8月10日にプロジェクトの終結が発表された。2015年1月、ヘイルズと21人の共同研究者は「ケプラー予想の形式的証明」と題された論文を公開した。