Optimal occupied-volume density

Open

KeplerMission.optimal_density_eq

by Minghui · Sep 27, 2026 · Mathlib c5ea003 (Lean v4.30.0)

discrete-geometrykeplersphere-packing

The supremum of the origin-centered occupied-volume upper densities of all unit-sphere packings in Euclidean three-space equals π/√18. The lower bound additionally requires the explicit FCC witness √2D₃, whose packing property and exact density are stated separately. The proved conditional supremum assembly exposes this input. This does not classify all attaining packings.

\sup_{V:\operatorname{Pack}(V)}\overline\delta(V)=\frac{\pi}{\sqrt{18}}.

Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §3 pp.5–6; Blueprint §1.2 (extended PDF pp.20–22), FCC witness; Lean-Eval KeplerConjecture.lean:Δ,kepler_conjecture.

Formalization note. Source-derived interface or explicitly identified analytic corollary; no proof of the target is supplied by defining its proposition.

Preamble

import Definitions.Def_Kepler_MissionContracts
set_option autoImplicit false

Formal statement

namespace KeplerMission
theorem optimal_density_eq : OptimalDensityGoal := by sorry
end KeplerMission

Source

Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1; §3 pp.5–6; Blueprint §1.2 (extended PDF pp.20–22), FCC witness; Lean-Eval KeplerConjecture.lean:Δ,kepler_conjecture; https://github.com/flyspeck/flyspeck/blob/1ce0353008eba83d3c76ae9a25c3c242e4802d53/text_formalization/general/the_main_statement.hl; https://publicationsthomashales.wordpress.com/wp-content/uploads/2016/03/densespherepackings.pdf

Read-back

What the Lean code literally says, in plain math · gpt-6

This defines, without proving, the equality $\sup\{D(V):V\subseteq\mathbb R^3,\ \forall u\neq v\in V,\ d(u,v)\geq2\}=\pi/\sqrt{18}$ , with $D(V)$ the real limsup of occupied open-unit-ball volume divided by observation-ball volume at the origin. Radii are real, infinite volumes convert to zero, division by zero gives zero, and real limsup uses the infimum of eventual upper bounds with the stated zero defaults. The outer real supremum is zero for an empty or unbounded-above set and is the least upper bound otherwise. Empty packings are allowed. This equality does not include existence of a maximizer or an ordinary limiting density.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph