Good Locally Testable Codes | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, `Good Locally Testable Codes`, Annals of Math, 203 (2) 2026. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2026-203-2-GoodLTCodes.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_2 (ρ : ℝ≥0) (hρ : ρ < 1) :
    ∃ q, ∃ κ ≠ 0, ∃ (n : ℕ → ℕ), ∃ (𝒞 : (i : ℕ) → GoodLTC.BinaryCode (n i)), GoodLTC.IsGood 𝒞 ∧
      ∀ i, Nonempty (GoodLTC.LTC q κ (𝒞 i)) ∧ rate (𝒞 i) ≥ ρ := byρ:ℝ≥0hρ:ρ < 1⊢ ∃ q κ, κ ≠ 0 ∧ ∃ n 𝒞, IsGood 𝒞 ∧ ∀ (i : ℕ), Nonempty (LTC q κ (𝒞 i)) ∧ rate (𝒞 i) ≥ ↑ρ
  sorryAll goals completed! 🐙