解法: ケプラー予想の形式的証明:HOL LightとIsabelleによるFlyspeckプロジェクト(2015年)

無限の空間全体を一度に考えようとする代わりに、ヘイルズは一つの球ずつに焦点を絞り、固定された距離までのごく近い隣人だけに注目する。もしこの小さな近傍が決して混みすぎることがないと示すことができ、詰め込み全体のあらゆる近傍が同じ局所的な規則に従うのであれば、無限の詰め込み全体が制御されたことになる——果樹園全体が健康であることを、一本一本の木とその最も近い隣の木だけを調べて確かめるようなものである。