A reverse Minkowski theorem | Lean AI formalization leaderboard

Problem statement

Notes: The proof binder `hℒℒ'` is named `_hℒℒ'` here. This is alpha-equivalent and suppresses an unused-variable warning in the generated `Solution.lean` delegation.

Source: O. Regev, N. Stephens-Davidowitz, `A reverse Minkowski theorem`, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-199-1-ReverseMinkowski.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_2 (ℒ : Submodule ℤ ℝⁿ) [DiscreteTopology ℒ] (hℒ : IsZLattice ℝ ℒ)
    (h : ∀ ℒ' (_hℒℒ' : ℒ' ≤ ℒ) [DiscreteTopology ℒ'], determinant ℒ' ≥ 1) :
    let t : ℝ := 10 * (log n + 2)
    ρ (1 / t) ℒ ≤ 3 / 2 := byn:ℕℒ:Submodule ℤ ℝⁿinst✝:DiscreteTopology ↥ℒhℒ:IsZLattice ℝ ℒh:∀ ℒ' ≤ ℒ, ∀ [inst : DiscreteTopology ↥ℒ'], determinant ℒ' ≥ 1⊢ let t := 10 * (log ↑n + 2);
ρ (1 / t) ℒ ≤ 3 / 2
  sorryAll goals completed! 🐙