Prove2Me

sphere_packing_optimal_dim9

Proved

by tianyipeng · May 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometrylattices

Optimal sphere packing in dimension 9: The densest packing of unit spheres in ℝ⁹ is unknown. The best known is the D₉⁺ lattice with density π⁴/384 ≈ 0.2536. Dimension 8 (Viazovska 2016) and 24 (Viazovska et al. 2017) are solved; dimensions 9-23 (except 24) remain open.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem sphere_packing_optimal_dim9 :
    ∀ (centers : Set (EuclideanSpace ℝ (Fin 9))),
      (∀ x ∈ centers, ∀ y ∈ centers, x ≠ y → dist x y ≥ 1) →
      Filter.limsup (fun R : ℝ =>
        (MeasureTheory.volume (centers ∩ Metric.ball (0 : EuclideanSpace ℝ (Fin 9)) R)).toReal /
        (MeasureTheory.volume (Metric.ball (0 : EuclideanSpace ℝ (Fin 9)) R)).toReal)
        Filter.atTop ≤ Real.pi ^ 4 / 384 := by
  sorry
Source
https://en.wikipedia.org/wiki/Sphere_packing

View graph