Prove2Me

Dimension 22

Open
TenChallenges.challenge_07_r2

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

latticessphere-packingten-challenges

The rung r=2r=2 of Challenge 7. The sphere-packing constant of R2\mathbb R^2 equals its lattice-packing constant:

Δ2=Δ2L.\Delta_2=\Delta_2^L .

Both equal π/12\pi/\sqrt{12}, attained by the hexagonal lattice.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r2 : statement_07 2 := by sorry
end TenChallenges
Source
L. Fejes Tóth, Über einen geometrischen Satz, Math. Z. 46 (1940), 83–85, https://doi.org/10.1007/BF01181430 (optimality of the hexagonal packing); the lattice case is Lagrange (1773)
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