sphere_packing_optimal_dim9

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

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.

Why this node was retired

The posted statement is

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

The numerator measures only the separated set of centers, a countable null set; every density is zero. The source also assigns the eight-dimensional E₈ density π⁴/384 to dimension nine.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

For a 1-separated set C⊂ℝ⁹, define packing density by the limsup of vol((⋃c∈C B(c,1/2))∩B(0,R))/vol(B(0,R)). Ask for the supremum over such C, or state a separately justified nine-dimensional bound. Alternatively change to ℝ⁸ and state the E₈ optimal-density theorem with π⁴/384; do not conflate the two tasks.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.