Prove2Me

optimal_sphere_packing_d3

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometryprovedsphere-packing

Kepler conjecture (proved by Hales-Ferguson 2005, formal proof 2017): The FCC/HCP lattice gives the densest sphere packing in ℝ³ with density π/(3√2) ≈ 0.7405. The formal Lean proof is part of the Flyspeck project.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem optimal_sphere_packing_d3 :
    ∀ (centers : Set (EuclideanSpace ℝ (Fin 3))),
      (∀ x ∈ centers, ∀ y ∈ centers, x ≠ y → dist x y ≥ 1) →
      Filter.limsup (fun R : ℝ =>
        (MeasureTheory.volume (centers ∩ Metric.ball 0 R)).toReal /
        (MeasureTheory.volume (Metric.ball (0 : EuclideanSpace ℝ (Fin 3)) R)).toReal)
      Filter.atTop ≤ Real.pi / (3 * Real.sqrt 2) := by
  sorry
Source
https://en.wikipedia.org/wiki/Kepler_conjecture

View graph