Hilbert's sixteenth problem: uniform bounds for limit cycles

Resolves the uniform boundedness assertion in Hilbert's sixteenth problem: the number of isolated periodic orbits of a real planar polynomial vector field is bounded by a finite constant depending only on its degree. For classical quintic Liénard systems, the exact maximum is two limit cycles. (Lean)

Manuscripts (2)

Uniform bounds for planar polynomial limit cycles

September 24, 2026 · source · cite as \cite{OAI:uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026}

For every degree, we prove that the number of isolated periodic orbits of a real planar polynomial vector field is bounded by a finite constant depending only on that degree. This establishes the uniform boundedness assertion in the second part of Hilbert's sixteenth problem. The proof uses separation of asymptotic expansions on nested complex domains and a finite-dimensional counting argument.

Two limit cycles for quintic Liénard systems

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:two-limit-cycles-for-quintic-lienard-systems-September-24-2026}

Every classical Liénard system \dot x=y-F(x), \dot y=-x, with F an arbitrary real polynomial of degree at most five, has at most two geometrically distinct isolated periodic orbits, and the bound is attained. This proves the degree-five case of the Lins Neto–de Melo–Pugh conjecture.

Result 143 · Dynamical systems and ergodic theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.