Dynamical systems and ergodic theory · Result 143

Hilbert's sixteenth problem: uniform bounds for limit cycles

2 papersLean

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.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Uniform bounds for planar polynomial limit cycles

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026,
  author = {{OpenAI}},
  title = {{Uniform bounds for planar polynomial limit cycles}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026/uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026.pdf}{OAI:uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026}},
  year = {2026}
}

Two limit cycles for quintic Liénard systems

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:two-limit-cycles-for-quintic-lienard-systems-September-24-2026,
  author = {{OpenAI}},
  title = {{Two limit cycles for quintic Li{\'e}nard systems}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/two-limit-cycles-for-quintic-lienard-systems-September-24-2026/two-limit-cycles-for-quintic-lienard-systems-September-24-2026.pdf}{OAI:two-limit-cycles-for-quintic-lienard-systems-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Two limit cycles for quintic Liénard systems

Scope

For the quintic Liénard system \(x'=y-F(x)\), \(y'=-x\), the formalized result proves that every real polynomial \(F\) of degree at most five yields at most two limit cycles, and that some such \(F\) yields exactly two. Limit cycles are isolated images of nonconstant periodic solutions. No sign, parity, hyperbolicity, or amplitude restriction is imposed.

Comparator links

Result	Comparator statement
Exact two-cycle bound for quintic Liénard systems	QuinticLienard.lean

Scope note on GitHub →