Det gir vedlikeholderne av Sphere Packing Project stor glede å kunngjøre en viktig milepæl i formaliseringsarbeidet: vi har nå et beklagefritt Lean-bevis for teoremet om at optimal sphere packing i R⁸ er E₈ gitterpakking. (1/9)