Galois groups of random integer polynomials and van der Waerden's Conjecture

Problem statement

Notes: Unavailable.

Source: M. Bhargava, `Galois groups of random integer polynomials and van der Waerden's Conjecture`, Annals of Math, 201 (2) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2025-201-2-vanDerWaerdenConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (n : ℕ) (hn : 3 ≤ n) :
    (fun H ↦ (vanDerWaerdenConjecture.E n H : ℝ)) =O[atTop] (fun H ↦ (H ^ (n - 1) : ℝ)) := byn:ℕhn:3 ≤ n⊢ (fun H => ↑(E n H)) =O[atTop] fun H => ↑H ^ (n - 1)
  sorryAll goals completed! 🐙