hilbert_16th_problem

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result hilbert_16th_problem is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Hilbert's 16th problem (second part, 1900): For polynomial vector fields (ẋ, ẏ) = (P(x,y), Q(x,y)) of degree n in ℝ², what is the maximum number H(n) of limit cycles? Even H(2) is unknown. Ilyashenko (2002) proved H(n) < ∞ for each fixed n but no uniform bound is known.

Why this node was retired

The posted statement is

import Mathlib

theorem hilbert_16th_problem :
    ∃ (H : ℕ → ℕ),
    ∀ (n : ℕ) (P Q : MvPolynomial (Fin 2) ℝ),
      P.totalDegree ≤ n → Q.totalDegree ≤ n →
      let field : ℝ × ℝ → ℝ × ℝ := fun xy =>
        (MvPolynomial.eval (fun i => if i = 0 then xy.1 else xy.2) P,
         MvPolynomial.eval (fun i => if i = 0 then xy.1 else xy.2) Q)
      (∃ cycles : Finset (Set (ℝ × ℝ)),
        cycles.card ≤ H n ∧
        ∀ (x0 : ℝ × ℝ), True) := by
  sorry

The conclusion contains ∃ cycles : Finset (Set (ℝ × ℝ)), cycles.card ≤ H n ∧ ∀ (x0 : ℝ × ℝ), True; the second conjunct is True, so the empty finset witnesses the existential and no limit cycle is ever required to be one.

What a faithful statement would require

cycles must be required to consist of the limit cycles of the given polynomial vector field, and the bound must be on their number.

No corrected replacement node exists yet.