S velkým potěšením oznamují významný milník ve formalizačním úsilí: nyní máme bez smutného Lean důkazu věty, že optimální balení koulí v R⁸ je E₈ mřížkové balení. (1/9)