É com grande prazer que os mantenedores do Projeto de Empacotamento de Esferas anunciam um marco importante no esforço de formalização: agora temos uma prova Lean sem desculpas do teorema de que o empacotamento de esferas ótimo em ℝ⁸ é o empacotamento da rede E₈. (1/9)