Klartag's construction of lattice sphere packings | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: Unavailable.

Informal solution: Unavailable.

theorem declaration uses `sorry`klartag_packing : ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ,
    let V := EuclideanSpace ℝ (Fin (n + 1))
    ∃ φ : V →ₗ[ℝ] V, let E := φ '' Metric.ball (0 : V) 1
      (MeasureTheory.volume E : EReal) = c * n ^ 2 ∧
      {v ∈ E | ∀ i, v i ∈ Set.range ((↑) : ℤ → ℝ)} = {0} := by⊢ ∃ c,
  0 < c ∧
    ∀ (n : ℕ),
      let V := EuclideanSpace ℝ (Fin (n + 1));
      ∃ φ,
        let E := ⇑φ '' Metric.ball 0 1;
        ↑(MeasureTheory.volume E) = ↑c * ↑n ^ 2 ∧ {v | v ∈ E ∧ ∀ (i : Fin (n + 1)), v.ofLp i ∈ Set.range Int.cast} = {0}
  sorryAll goals completed! 🐙