Motivation

The sphere packing problem asks for the largest fraction of $\mathbb R^d$ that can be covered by non-overlapping unit balls. The densest packings known in most dimensions are lattice packings, whose centres form a lattice, and for $d\in\{1,2,3,8,24\}$ a lattice packing is known to be optimal among all packings. But in several dimensions, $d=10$ being the first, the densest packing known is not a lattice packing and is denser than the best lattice packing known (Conway–Sloane 1999). Whether the sphere-packing constant and the lattice-packing constant agree in every dimension is open; the answer may well be negative, and this challenge is a question rather than a conjecture.

Timeline.

• 1611 — Kepler asserts that the face-centred cubic packing is densest in dimension $3$.
• 1773/1831 — Lagrange and Gauss show that the hexagonal and face-centred cubic lattices are the densest lattice packings in dimensions $2$ and $3$.
• 1910/1940 — Thue and Fejes Tóth prove the hexagonal packing optimal among all packings of the plane (Fejes Tóth 1940).
• 1998/2005 — Hales proves the Kepler conjecture; the Flyspeck project completes a formal proof in HOL Light and Isabelle in 2014 (Hales 2005, Hales et al. 2017).
• 2016 — Viazovska proves that the $E_8$ lattice packing is optimal in dimension $8$; Cohn, Kumar, Miller, Radchenko and Viazovska prove that the Leech lattice packing is optimal in dimension $24$ (Viazovska 2017, Cohn–Kumar–Miller–Radchenko–Viazovska 2017).
• 2024–2026 — The Sphere Packing project formalizes Viazovska's theorem in Lean 4, with the final steps completed in 2026 (Sphere Packing in Lean).

Setting

Fix $d\ge 1$ and equip $\mathbb R^d$ with the Euclidean distance and Lebesgue measure $\mathrm{Vol}$; $B(x,\rho)$ is the open ball of radius $\rho$ about $x$. A unit packing is a set $C\subseteq\mathbb R^d$ of centres with $\|x-y\|\ge 2$ for all distinct $x,y\in C$, so the open unit balls about the points of $C$ are pairwise disjoint. Its upper density is

$$\bar\delta(C) := \limsup_{R\to\infty}\ \frac{\mathrm{Vol}\big(\bigcup_{x\in C}B(x,1)\cap B(0,R)\big)}{\mathrm{Vol}(B(0,R))}.$$

The sphere-packing constant $\Delta_d$ is the supremum of $\bar\delta(C)$ over all unit packings $C$ of $\mathbb R^d$. A lattice packing is a unit packing $L$ that is an additive subgroup of $\mathbb R^d$ spanning $\mathbb R^d$; the separation condition forces $L$ to be discrete, hence a full-rank lattice. The lattice-packing constant $\Delta_d^L$ is the supremum of $\bar\delta(L)$ over lattice packings. Trivially $\Delta_d^L\le\Delta_d$. For $r\in\mathbb N$ let

$$\mathrm{SP}(r):\quad \Delta_r=\Delta_r^L .$$

Formalization targets

Goal

$$\forall r\in\mathbb N:\quad \Delta_r=\Delta_r^L .$$

A disproof, exhibiting a dimension in which some non-lattice packing beats every lattice packing, is as welcome as a proof.

Rungs

$\mathrm{SP}(r)$ is known for $r\in\{1,2,3,8,24\}$; $\mathrm{SP}(4)$ is the first open rung. In dimensions $4$ to $7$ the densest lattice packings are known ($D_4$, $D_5$, $E_6$, $E_7$; Korkine–Zolotarev, Blichfeldt), so only the general constant is missing there.

Significance

The equality $\Delta_d=\Delta_d^L$ is the statement that lattices suffice for sphere packing. In dimension $3$ it is the Kepler conjecture (since $\Delta_3^L$ was known from Gauss), in dimensions $8$ and $24$ it is the content of the Fields-medal work of Viazovska and her coauthors. A counterexample would be a dimension in which non-lattice packings are provably better, which is expected in high dimensions but not proved in any.

The rungs $r=8$ and $r=24$ have machine-checked proofs in the Lean Sphere Packing project, in its own definitions; transferring them to the definitions here means proving that the two formalizations of density agree, which is a substantial but well-defined task. The rung $r=3$ has a formal proof in HOL Light and Isabelle (Flyspeck), not in Lean. The rungs $r=1$ and $r=2$ have no machine-checked proof; $r=1$ is an exercise once the density of a packing of the line is computed, while $r=2$ needs the Thue–Fejes Tóth theorem.

Difficulty

Upper bounds on $\Delta_d$ are the hard direction: the known proofs use the linear-programming bound of Cohn and Elkies and a magic modular form (dimensions $8$, $24$), or a computer-assisted analysis of local configurations (dimension $3$). The lattice constant is comparatively tractable, which is why the question stands exactly where the general constant is unknown. The naive approach, that the densest packing must have the symmetry of a lattice, is unfounded: in dimension $10$ Best's packing is denser than any known lattice, and in high dimensions the best known packings are periodic but not lattice.

Formalization scope

Points are EuclideanSpace ℝ (Fin d) with its volume (the Lebesgue measure through Mathlib's Haar measure), and a packing is a set C : Set (EuclideanSpace ℝ (Fin d)). IsUnitPacking C requires $2\le\mathrm{dist}(x,y)$ for distinct $x,y\in C$. upperDensity C : ℝ≥0∞ is limsup over $R\to\infty$ (Filter.atTop on $\mathbb R$) of the quotient of extended nonnegative reals above; spherePackingConstant d is the indexed supremum ⨆ over all sets $C$ satisfying IsUnitPacking C, and latticePackingConstant d the supremum over AddSubgroups $L$ of the space whose carrier is a unit packing and whose real span is the whole space. The rung statement_07 r is the equality of the two constants in ℝ≥0∞, and the goal is ∀ r, statement_07 r.

No trivialising reading: densities are at most $1$, the supremum over the empty family is $0$, and for $d=0$ both constants trivially coincide. Densities are extended nonnegative reals, so no real-valuedness hypotheses are needed; the quotient uses the convention of ℝ≥0∞ division, harmless since $\mathrm{Vol}(B(0,R))>0$ for $R>0$. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: the inequality $\Delta_d^L\le\Delta_d$, the bound $\Delta_d\le 1$, periodification lemmas, the density of a lattice packing as $\mathrm{Vol}(B(0,1))/\mathrm{covol}(L)$, and the bridge to the Sphere Packing project's definitions.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 7).
• J. H. Conway, N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Springer, 1999. https://doi.org/10.1007/978-1-4757-6568-7
• L. Fejes Tóth, Über einen geometrischen Satz, Math. Z. 46 (1940), 83–85. https://doi.org/10.1007/BF01181430
• T. C. Hales, A proof of the Kepler conjecture, Ann. of Math. 162 (2005), 1065–1185. https://doi.org/10.4007/annals.2005.162.1065
• T. Hales et al., A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2. https://doi.org/10.1017/fmp.2017.1
• M. S. Viazovska, The sphere packing problem in dimension 8, Ann. of Math. 185 (2017), 991–1015. https://doi.org/10.4007/annals.2017.185.3.7
• H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, The sphere packing problem in dimension 24, Ann. of Math. 185 (2017), 1017–1033. https://doi.org/10.4007/annals.2017.185.3.8
• H. Cohn, N. Elkies, New upper bounds on sphere packings I, Ann. of Math. 157 (2003), 689–714. https://doi.org/10.4007/annals.2003.157.689
• The Sphere Packing project, Progress in formalizing sphere packing in dimension 8, 2026. https://arxiv.org/abs/2604.23468 — code: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean