これは、球面パッキングプロジェクトの管理者にとって、形式化作業における重要な節目を発表できることを大変嬉しく思います。すなわち、R⁸における最適な球面詰め込みがE₈格子詰めであるという定理の、すごく無料のリーン証明が得られたということです。(1/9)