面心立方格子が最密充填の一つだということは、たしか高校の教科書にも載っている。でもこれが証明されたのは 1998 年らしい。そんなに最近の結果だったんだ。ただし、規則的な配置という条件のもとではガウスが証明している。教科書で古典的な結果のように扱われているのは、暗黙にガウスの証明を指しているんだろう。
Hales による証明は、紙 300 ページに加えてコンピュータによる最適化の結果が付属する長大なものらしい。Hales はその後、証明を定理証明器によって検証するプロジェクトに取り組み、完了したのはなんと 2014 年だとか。