New large value estimates for Dirichlet polynomials | Lean AI formalization leaderboard

Problem statement

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

Source: L. Guth and J. Maynard, `New large value estimates for Dirichlet polynomials`, Annals of Math, 203 (2) 2026. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2026-203-2-LargeValueEstimates.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 : ∃ o : ℝ → ℝ, o =o[Filter.atTop] (1 : ℝ → ℝ) ∧
    ∀ (b : ℕ → ℂ) (_hb : ∀ n, ‖b n‖ ≤ 1) (N : ℕ) (V : ℝ) (T : ℝ) (R : ℕ) (t : Fin R → ℝ),
    N > 0 → V > 0 → T > 1 → -- these assumptions are necessary but not stated in the paper
    (∀ i j, i ≠ j → |t i - t j| ≥ 1) → (∀ i, t i ∈ Set.Icc 0 T) →
    (∀ r, ‖∑ n ∈ Finset.Icc N (2 * N), b n * n ^ (I * t r)‖ ≥ V) →
    R ≤ T ^ (o T) * bound N V T := by⊢ ∃ o,
  o =o[Filter.atTop] 1 ∧
    ∀ (b : ℕ → ℂ),
      (∀ (n : ℕ), ‖b n‖ ≤ 1) →
        ∀ (N : ℕ) (V T : ℝ) (R : ℕ) (t : Fin R → ℝ),
          N > 0 →
            V > 0 →
              T > 1 →
                (∀ (i j : Fin R), i ≠ j → |t i - t j| ≥ 1) →
                  (∀ (i : Fin R), t i ∈ Set.Icc 0 T) →
                    (∀ (r : Fin R), ‖∑ n ∈ Finset.Icc N (2 * N), b n * ↑n ^ (I * ↑(t r))‖ ≥ V) →
                      ↑R ≤ T ^ o T * bound N V T
  sorryAll goals completed! 🐙