Prove2Me

Dimension 2424

Open
TenChallenges.challenge_07_r24

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

latticessphere-packingten-challenges

The rung r=24r=24 of Challenge 7. The sphere-packing constant of R24\mathbb R^{24} equals its lattice-packing constant:

Δ24=Δ24L.\Delta_{24}=\Delta_{24}^L .

Both equal π12/12!\pi^{12}/12!, attained by the Leech lattice.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r24 : statement_07 24 := by sorry
end TenChallenges
Source
H. Cohn, A. Kumar, S. D. Miller, D. Radchenko, M. Viazovska, The sphere packing problem in dimension 24, Ann. of Math. 185 (2017), 1017–1033, https://doi.org/10.4007/annals.2017.185.3.8
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