Prove2Me

Dimension 44

Open
TenChallenges.challenge_07_r4

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

latticessphere-packingten-challenges

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

Δ4=Δ4L.\Delta_4=\Delta_4^L .

The lattice constant is π2/16\pi^2/16, attained by D4D_4; whether a non-lattice packing is denser is open.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r4 : statement_07 4 := by sorry
end TenChallenges
Source
Open; the densest lattice packing of R4\mathbb R^4 is D4D_4 (Korkine and Zolotarev, 1872), see J. H. Conway, N. J. A. Sloane, Sphere Packings, Lattices and Groups, 3rd ed., Chapter 1, Table 1.2, 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