Prove2Me

Dimension 33

Open
TenChallenges.challenge_07_r3

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

latticessphere-packingten-challenges

The rung r=3r=3 of Challenge 7: the Kepler conjecture. The sphere-packing constant of R3\mathbb R^3 equals its lattice-packing constant:

Δ3=Δ3L.\Delta_3=\Delta_3^L .

Both equal π/18\pi/\sqrt{18}, attained by the face-centred cubic lattice.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r3 : statement_07 3 := by sorry
end TenChallenges
Source
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; formal proof in T. Hales et al., A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), https://doi.org/10.1017/fmp.2017.1
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

  • Endorsed by utkuokur · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph