Es bereitet den Betreuern des Sphere Packing Project große Freude, einen wichtigen Meilenstein im Formalisierungsprozess bekannt zu geben: Wir haben jetzt einen fehlerfreien Lean-Beweis des Theorems, dass die optimale Kugelpackung in ℝ⁸ die E₈-Gitterpackung ist. (1/9)