Het geeft de beheerders van het Sphere Packing Project veel plezier om een belangrijke mijlpaal in de formalisatie-inspanning aan te kondigen: we hebben nu een spijtvrije Lean-bewijs van de stelling dat de optimale bolverpakking in ℝ⁸ de E₈ roosterverpakking is. (1/9)