Prove2Me

Dimension 11

Proved
TenChallenges.challenge_07_r1

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

latticessphere-packingten-challenges

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

Δ1=Δ1L.\Delta_1=\Delta_1^L .

Both equal 11, attained by the lattice 2Z2\mathbb Z.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r1 : statement_07 1 := by sorry
end TenChallenges
Source
Elementary; J. H. Conway, N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Chapter 1, https://doi.org/10.1007/978-1-4757-6568-7
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