Prove2Me

Dimension 88

Open
TenChallenges.challenge_07_r8

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

latticessphere-packingten-challenges

The rung r=8r=8 of Challenge 7: Viazovska's theorem. The sphere-packing constant of R8\mathbb R^8 equals its lattice-packing constant:

Δ8=Δ8L.\Delta_8=\Delta_8^L .

Both equal π4/384\pi^4/384, attained by the E8E_8 lattice.

Preamble
import Definitions.Def_TenChallenges_Challenge_07
Formal statement
namespace TenChallenges
theorem challenge_07_r8 : statement_07 8 := by sorry
end TenChallenges
Source
M. S. Viazovska, The sphere packing problem in dimension 8, Ann. of Math. 185 (2017), 991–1015, https://doi.org/10.4007/annals.2017.185.3.7; Lean formalization: https://arxiv.org/abs/2604.23468
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