Van der Waerden's conjecture on Galois groups

DefinitionMonic integer polynomials whose Galois group is not \(S_n\)#✓fully proved

For natural numbers \(n\) and \(H\), \(E_n(H)\) is the number of monic polynomials \(f(x) = x^n + a_1 x^{n-1} + \dots + a_n\) of degree \(n\) with integer coefficients and \(|a_i| \le H\) for \(i = 1, \dots, n\) whose Galois group over \(\mathbb{Q}\) has order less than \(n!\), that is, is not the full symmetric group \(S_n\).

def E (n H : ℕ) : ℕ :=
  {p : ℤ[X] | p.Monic ∧ p.degree = n ∧ (∀ i < n, |p.coeff i| ≤ H) ∧
    Nat.card (p.map (algebraMap ℤ ℚ)).Gal < n.factorial}.ncard

Used by 1

Used byVan der Waerden's conjecture (Bhargava)

TheoremVan der Waerden's conjecture (Bhargava)#●ready to prove

For every natural number \(n \ge 3\) there is a constant \(C\) such that \(E_n(H) \le C H^{n-1}\) for all sufficiently large natural numbers \(H\), where \(E_n(H)\) is the number of monic polynomials of degree \(n\) with integer coefficients, all non-leading coefficients of absolute value at most \(H\), whose Galois group over \(\mathbb{Q}\) has order less than \(n!\).

The degree restriction is necessary: the statement is false for \(n = 2\).

public theorem_wanted theorem_1 (n : ℕ) (hn : 3 ≤ n) :
    (fun H ↦ (E n H : ℝ)) =O[atTop] (fun H ↦ (H ^ (n - 1) : ℝ))

Sources

• 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. Problem annals_van_der_waerden_conjecture of the lean-eval benchmark.

Uses 1

Statement usesMonic integer polynomials whose Galois group is not \(S_n\)

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.