FormalConjectures/HilbertProblems/17.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 3 contain sorry, 0 declared as axioms

Hilbert's 17th problem

Let $f(x_1, \dots, x_n)$ be a multivariable polynomial with real coefficients that takes only nonnegative values for all real inputs. Hilbert's 17th problem asks whether there exist rational functions $g_1, \dots, g_m$ such that $f = g_1^2 + g_2^2 + \cdots + g_m^2$. Resolved affirmatively by Artin in 1927. References:

Imports (1)
  1. theorem Hilbert17.hilbert_17th_problem Hilbert's 17th problem: every non-negative multivariate polynomial is a sum of squares of rational functions sorry line 43 source

    Source documentation

    Hilbert's 17th problem: every non-negative multivariate polynomial is a sum of squares of rational functions.

    depends on sorry what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, MvPolynomial, Fin, Real, LE.le, RingHom, Finsupp, MvPolynomial.eval, Exists, MvRatFunc, Eq, nonZeroDivisors, Algebra.algebraMap, Finset.sum, Finset.univ, HPow.hPow

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    80 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem hilbert_17th_problem {n : ℕ} (hn : 0 < n) (f : MvPolynomial (Fin n) ℝ)
    (h : ∀ x : Fin n → ℝ, 0 ≤ f.eval x) :
    ∃ (m : ℕ) (g : Fin m → MvRatFunc (Fin n) ℝ), algebraMap _ _ f = ∑ i, (g i) ^ 2 := by
…

    Mentions: Hilbert17.f, MvRatFunc

  2. def Hilbert17.f The statement is false in general if we restrict to polynomials line 53 source

    Source documentation

    The statement is false in general if we restrict to polynomials. The polynomial (by Motzkin) $f(x, y) = x^4 y^2 + x^2 y^4 - 3 x^2 y^2 + 1$ takes only nonnegative values but cannot be written as a sum of squares of polynomials.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MvPolynomial, Fin, OfNat.ofNat, Nat, Real

    Proof uses: HAdd.hAdd, Finsupp, HSub.hSub, HMul.hMul, HPow.hPow, MvPolynomial.X

    37 instances, coercions and auxiliary constants left out.

    noncomputable def f : MvPolynomial (Fin 2) ℝ :=
…
  3. theorem Hilbert17.f_nonneg The Motzkin polynomial is non-negative everywhere line 59 source

    Source documentation

    The Motzkin polynomial is non-negative everywhere.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, RingHom, MvPolynomial, Fin, Nat.succ, Nat, Finsupp, MvPolynomial.eval, Matrix.vecCons, Matrix.vecEmpty, Hilbert17.f

    Proof uses: Eq.mpr, HAdd.hAdd, HSub.hSub, HMul.hMul, HPow.hPow, id, Eq, congrArg, Eq.trans, MvPolynomial.X, map_add, congr, map_sub, map_mul, map_pow, congrFun', MvPolynomial.eval_X, Matrix.cons_val_fin_one, MvPolynomial.eval_ofNat, map_one and 95 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

    theorem f_nonneg : ∀ x y : ℝ, 0 ≤ f.eval ![x, y] := by
…
  4. theorem Hilbert17.f_not_sum_of_squares The Motzkin polynomial cannot be written as a sum of squares of polynomials sorry line 73 source

    Source documentation

    The Motzkin polynomial cannot be written as a sum of squares of polynomials.

    depends on sorry what this means

    Statement uses: Not, Exists, Nat, LT.lt, OfNat.ofNat, Fin, MvPolynomial, Real, Eq, Hilbert17.f, Finset.sum, Finsupp, Finset.univ, HPow.hPow

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    30 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem f_not_sum_of_squares :
    ¬∃ (n : ℕ) (hn : 0 < n) (S : Fin n → MvPolynomial (Fin 2) ℝ), f = ∑ i, S i ^ 2 := by
…

    Mentions: Hilbert17.f

  5. def Hilbert17.Hilbert17thProblemHomogenousPoly Documented declaration: Hilbert17thProblemHomogenousPoly line 85 source

    Source documentation

    For the polynomial version, Hilbert showed that every nonnegative homogeneous polynomial in $n$ variables of degree $2d$ can be written as a sum of squares of polynomials if and only if

    • $n = 1$
    • $n = 2$
    • $d = 1$
    • $(n, d) = (3, 2)$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: MvPolynomial, Fin, Real, MvPolynomial.IsHomogeneous, HMul.hMul, OfNat.ofNat, LE.le, RingHom, Finsupp, MvPolynomial.eval, Exists, Eq, Finset.sum, Finset.univ, HPow.hPow

    25 instances, coercions and auxiliary constants left out.

    def Hilbert17thProblemHomogenousPoly (n d : ℕ) : Prop :=
…
  6. theorem Hilbert17.Hilbert17thProblemHomogenousPoly_zero_left line 91 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Hilbert17.Hilbert17thProblemHomogenousPoly, OfNat.ofNat

    Proof uses: MvPolynomial, Fin, Real, MvPolynomial.IsHomogeneous, HMul.hMul, LE.le, RingHom, Finsupp, MvPolynomial.eval, Exists.intro, Exists, Eq, Finset.sum, Finset.univ, HPow.hPow, MvPolynomial.C, Real.sqrt, MvPolynomial.coeff, Ne, MvPolynomial.totalDegree and 30 more

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  7. theorem Hilbert17.Hilbert17thProblemHomogenousPoly_zero_right line 100 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Hilbert17.Hilbert17thProblemHomogenousPoly, OfNat.ofNat

    Proof uses: MvPolynomial, Fin, Real, MvPolynomial.IsHomogeneous, HMul.hMul, LE.le, RingHom, Finsupp, MvPolynomial.eval, Eq, Ne, Or, Exists, Finset.sum, Finset.univ, HPow.hPow, eq_or_ne, Exists.intro, of_eq_true, Eq.trans and 41 more

    69 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

  8. theorem Hilbert17.hilbert_17th_problem_poly Hilbert's 17th problem for homogeneous polynomials: characterization of dimensions and degrees where non-negative polynomials are sums of squares of polynomials sorry line 115 source

    Source documentation

    Hilbert's 17th problem for homogeneous polynomials: characterization of dimensions and degrees where non-negative polynomials are sums of squares of polynomials.

    depends on sorry what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Iff, Hilbert17.Hilbert17thProblemHomogenousPoly, Or, Eq, And

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem hilbert_17th_problem_poly {n d : ℕ} (hn : 0 < n) (hd : 0 < d) :
    Hilbert17thProblemHomogenousPoly n d ↔ n = 1 ∨ n = 2 ∨ d = 1 ∨ n = 3 ∧ d = 2 := by
…

    Mentions: Hilbert17.Hilbert17thProblemHomogenousPoly