С большим удовольствием мы, поддерживающие проект Sphere Packing, объявляем о значительном достижении в усилиях по формализации: у нас теперь есть доказательство теоремы о том, что оптимальная упаковка сфер в ℝ⁸ — это упаковка решетки E₈, свободная от извинений. (1/9)