Enumerating number fields | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: J.-M. Couveignes, `Enumerating number fields`, Annals of Math, 192 (2) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2020-192-2-EnumeratingNumberFields.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1 (Number fields have small models):

There exists a positive constant `Q` such that the following is true. Let `K` be a number field
of degree `n ≥ Q` and root discriminant `δ` over `ℚ`. Then there exist integers `r ≤ Q log n` and
`d ≤ Q log n` such that `(d + r) choose r ≤ Q n log n`, and there exist `r` polynomials
`E₁, ..., Eᵣ` of degree `≤ d` in `ℤ[x₁, ..., xᵣ]` all having coefficients bounded in absolute value
by `(n δ) ^ (Q log n)` such that the (smooth and zero-dimensional affine) scheme with equations
`E₁ = ... = Eᵣ = 0` and `det (∂Eᵢ/∂xⱼ) ≠ 0` contains `Spec K` as one of its irreducible components.
-/
theorem declaration uses `sorry`theorem_1 : ∃ Q > 0, ∀ n ≥ Q, ∀ K : NumberFieldOfDegree n, ∃ (r d : ℕ),
    r ≤ Q * log n ∧ d ≤ Q * log n ∧ (d + r).choose r ≤ Q * n * log n ∧
      ∃ E : Fin r → MvPolynomial (Fin r) ℤ, (∀ i, (E i).totalDegree ≤ d) ∧
        (∀ i j, |(E i).coeff j| ≤ (n * rootDiscr K) ^ (Q * log n)) ∧
          letI X := nonsingularOpen fun i ↦ (E i).map (algebraMap ℤ ℚ)
          ∃ Z, ∃ hZ : Z ∈ irreducibleComponents X,
            Nonempty (X.irreducibleComponent Z hZ ≅ Spec (.of K)) := by⊢ ∃ Q > 0,
  ∀ n ≥ Q,
    ∀ (K : NumberFieldOfDegree n),
      ∃ r d,
        ↑r ≤ ↑Q * log ↑n ∧
          ↑d ≤ ↑Q * log ↑n ∧
            ↑((d + r).choose r) ≤ ↑Q * ↑n * log ↑n ∧
              ∃ E,
                (∀ (i : Fin r), (E i).totalDegree ≤ d) ∧
                  (∀ (i : Fin r) (j : Fin r →₀ ℕ), ↑|(E i).coeff j| ≤ (↑n * rootDiscr K.carrier) ^ (↑Q * log ↑n)) ∧
                    ∃ Z,
                      ∃ (hZ :
                        Z ∈
                          irreducibleComponents ↥(nonsingularOpen fun i => (MvPolynomial.map (algebraMap ℤ ℚ)) (E i))),
                        Nonempty
                          ((nonsingularOpen fun i => (MvPolynomial.map (algebraMap ℤ ℚ)) (E i)).irreducibleComponent Z
                              hZ ≅
                            Spec ↧K.carrier)
  sorryAll goals completed! 🐙

/--
Statement of Theorem 2 (Number fields with bounded discriminant):

There exists a positive constant `Q` such that the following is true. Let `n ≥ Q` be an integer.
Let `H ≥ 1` be an integer. The number of isomorphism classes of number fields
with degree `n` and discriminant `≤ H` is `≤ n^(Q n log^3 n) H^(Q log^3 n)`.
-/
theorem declaration uses `sorry`theorem_2 : ∃ Q > 0, ∀ n ≥ Q, ∀ H ≥ 1,
    (Nat.card (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H) : ℝ) ≤
      n ^ (Q * n * log n ^ 3) * H ^ (Q * log n ^ 3) := by⊢ ∃ Q > 0,
  ∀ n ≥ Q,
    ∀ H ≥ 1,
      ↑(Nat.card (NumberFieldOfBoundedDiscriminantUpToIsomorphism n H)) ≤
        ↑n ^ (↑Q * ↑n * log ↑n ^ 3) * ↑H ^ (↑Q * log ↑n ^ 3)
  sorryAll goals completed! 🐙