Kepler conjecture

AbbreviationEuclidean space for sphere packings#✓fully proved

For a natural number \(d\), \(\mathbb{R}^d\) denotes the \(d\)-dimensional real Euclidean space: \(d\)-tuples of real numbers with the Euclidean norm.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

Used by 4

Used byCovered fraction of a ball · Density of a sphere packing · Unit sphere packing · Optimal sphere packing density

DefinitionUnit sphere packing#✓fully proved

For a natural number \(d\), a set \(X \subseteq \mathbb{R}^d\) is the centre set of a unit sphere packing if the open balls of radius \(1\) centred at any two distinct points of \(X\) are disjoint.

def IsPacking {d : ℕ} (X : Set (E d)) : Prop :=
  X.Pairwise (fun x y => Disjoint (Metric.ball x 1) (Metric.ball y 1))

Uses 1 · Used by 1

Statement usesEuclidean space for sphere packings

Used byOptimal sphere packing density

DefinitionCovered fraction of a ball#✓fully proved

For a natural number \(d\), a set \(X \subseteq \mathbb{R}^d\) and a real number \(R\), the covered fraction of \(X\) at radius \(R\) is

\[\frac{\operatorname{vol}\bigl(B_R(0) \cap \bigcup_{x \in X} B_1(x)\bigr)} {\operatorname{vol}(B_R(0))},\]

where \(B_r(y)\) is the open ball of radius \(r\) about \(y\) and \(\operatorname{vol}\) is Lebesgue measure; it equals \(0\) when \(R \le 0\).

noncomputable def coveredFraction {d : ℕ} (X : Set (E d)) (R : ℝ) : ℝ :=
  (volume ((⋃ x ∈ X, Metric.ball x 1) ∩ Metric.ball (0 : E d) R)).toReal /
    (volume (Metric.ball (0 : E d) R)).toReal

Uses 1 · Used by 1

Statement usesEuclidean space for sphere packings

Used byDensity of a sphere packing

DefinitionDensity of a sphere packing#✓fully proved

For a natural number \(d\), the density of a set \(X \subseteq \mathbb{R}^d\) is the limit superior, as \(R \to \infty\), of the covered fraction of \(X\) at radius \(R\): the fraction of the open ball of radius \(R\) about the origin covered by the open unit balls centred at points of \(X\).

noncomputable def density {d : ℕ} (X : Set (E d)) : ℝ :=
  Filter.limsup (coveredFraction X) Filter.atTop

Uses 2 · Used by 1

Statement usesEuclidean space for sphere packings · Covered fraction of a ball

Used byOptimal sphere packing density

DefinitionOptimal sphere packing density#✓fully proved

For a natural number \(d\), \(\Delta(d)\) is the supremum of the densities of all unit sphere packings in \(\mathbb{R}^d\).

noncomputable def Δ (d : ℕ) : ℝ :=
  sSup {δ : ℝ | ∃ X : Set (E d), IsPacking X ∧ density X = δ}

Uses 3 · Used by 1

Statement usesEuclidean space for sphere packings · Unit sphere packing · Density of a sphere packing

Used byKepler conjecture

TheoremKepler conjecture#●ready to prove

Let \(\Delta(3)\) be the supremum of the densities of all unit sphere packings in \(\mathbb{R}^3\). Then \(\Delta(3) = \pi / \sqrt{18}\).

public theorem_wanted kepler_conjecture : Δ 3 = Real.pi / Real.sqrt 18

Sources

• Kepler conjecture 1611 (J. Kepler, Strena seu de Nive Sexangula); proof T. Hales, 'A proof of the Kepler conjecture', Ann. of Math. (2) 162 (2005) 1065–1185; formal verification in HOL Light + Isabelle by the Flyspeck project (T. Hales et al., completed August 2014), Forum Math. Pi 5 (2017) e2. Wiedijk-1000 #209; listed as §96 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem kepler_conjecture of the lean-eval benchmark.

Uses 1

Statement usesOptimal sphere packing density

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.