A ceiling on limit cycles?

The claims, in plain words

In a planar polynomial vector field, the velocity at each point (x, y) is given by polynomials P and Q. Some orbits close up into loops, and a loop with no other closed orbit nearby is a limit cycle: neighbouring orbits spiral toward it or away from it. The van der Pol oscillator has exactly one. In 1900 Hilbert asked, in the second part of his sixteenth problem, for the maximum number and arrangement of limit cycles of polynomial systems of a given degree.

As the first paper explains, two finiteness assertions must be distinguished. Individual finiteness, for one fixed system, was claimed by Dulac in 1923; after a gap was found, Écalle and Ilyashenko developed proofs using complex and asymptotic analysis of return maps, and a 2025 paper by Yeung identifies an obstruction in one step of Ilyashenko’s argument, which the paper says is not a counterexample. Uniform boundedness asks for one bound depending only on the degree, and “even finiteness for every member of a family does not by itself bound the numbers occurring as its coefficients vary.” Partial results controlled cycles born from a focus, near elementary loops through saddles in generic families, or in an infinitesimal version with Abelian integrals. As far as we know, no uniform bound was known even for quadratic systems; the paper itself does not call the problem open.

Result 143 is two OpenAI preprints, both dated September 24, 2026. The first (160 pages) claims that for each degree d there is a finite B(d) such that every real planar polynomial vector field of degree at most d has at most B(d) limit cycles in the whole plane, with “no restriction on the coefficients, the locations of the cycles, or their stability.” It calls this “a positive resolution of the uniform boundedness assertion in the second part of Hilbert’s sixteenth problem.” The second (40 pages) claims that the classical Liénard oscillator ẋ = y − F(x), ẏ = −x with F of degree at most five has at most two limit cycles, and that two occur, with no sign or parity assumptions on F. That settles the degree-five case of the conjecture of Lins Neto, de Melo and Pugh (at most ⌊(n − 1)/2⌋ cycles when F has degree n), which has counterexamples in degrees six and seven; Rychkov had handled odd quintics in 1975, and the paper calls general degree five “undecided” before this work.

What it doesn’t claim

A number. The first paper “does not furnish an effective formula for B(d)” and gives no value for any degree, not even 2. It does not address the arrangement of the cycles, or the first part of Hilbert’s problem, about real algebraic curves. It does not assume individual finiteness, and it does not claim to repair or refute earlier proofs of it. The second paper covers only the classical Liénard form with restoring force exactly x and F of degree at most five; its two-cycle example, ε(4x − (20/3)x³ + (8/5)x⁵), is proved for some small ε > 0, not a specific value. The two papers do not cite each other, and the first gives no value of B(5) that would imply the second.

Where it stands

Posted as preprints

OpenAI, two preprints, 160 and 40 pages, dated September 24, 2026

Peer reviewed

Not yet

Checked in Lean

Only the quintic Liénard theorem. The uniform bound is not formalized

Last checked October 19, 2026. Neither preprint has been revised. OpenAI published a Lean formalization of the quintic Liénard theorem, at most two limit cycles for every F of degree at most five and exactly two for some, added to the repository in its initial commit on October 6, 2026 (comparator statement; 146 files and 16,659 lines, with no unproved steps that we could find). We have not run the check. The uniform bound, the headline claim, has no Lean formalization anywhere in the repository. Neither paper is among those OSVerify reviewed, and we have seen no expert review.

How the proofs go

1. What has to be counted. Any finite set of cycles can be shrunk into a fixed square without changing the degree, and a small rotation V + μ(−Q, P) of the field produces at least as many hyperbolic cycles, which nearby orbits approach or leave at a definite rate.
2. Finitely many ways around. A subanalytic preparation cuts the square into pieces whose number depends only on the degree. A periodic orbit crosses each transverse cut at most once, so every cycle, apart from a bounded number running along the cuts, is a closed word of boundedly many passages from a finite alphabet. Passages near saddles are the hard part: with a tiny eigenvalue, the time spent near the saddle can blow up while the contraction stays mild.
3. Matching and counting. For each word, matching equations say that each passage ends where the next begins. A hyperbolic cycle gives nondegenerate solutions, and within each chart different hyperbolic cycles lie on different connected components, so it is enough to bound the number of components uniformly in the coefficients. That count needs every derived system to have finitely many isolated solutions even when all its variables move freely.
4. Separation. When solutions escape to infinity, each function is expanded as a tree of exponentially small terms on nested complex domains, and either every coefficient vanishes and the function is exactly zero, or its first nonzero term dominates. The final bound is a finite sum whose terms the proof never computes.
5. Two arches (the Liénard paper). Each periodic orbit crosses the y-axis once in each direction; with u = x²/2 its two halves become arches, and a cycle is a width at which both arches have the same midpoint. A quadratic fit of each arch and a model inequality, transported along the width, split the problem into four cases by the signs of the x and x³ coefficients (after making the x⁵ coefficient nonnegative): one allows no cycle, two allow at most one, and in the last the mismatch times a positive weight can only fall and then rise, so it vanishes at most twice.

The numbers in the video

• Van der Pol, ẋ = y − (x³/3 − x), ẏ = −x: orbits from inside and outside approach one cycle of amplitude 2.0086 and period 6.6633.
• The quintic example at ε = 1/10: an inner repelling cycle of amplitude about 1.0009 and an outer attracting cycle of amplitude about 2.0008; the averaged energy change is −πs²(s² − 1)(s² − 4).
• A non-odd quintic of the two-cycle case, F = 0.1914x + 0.1279x² − 0.4722x³ − 0.113x⁴ + 0.1306x⁵: the mismatch has zeros at widths 0.798 and 2.142, one repelling and one attracting cycle.
• A double cycle at radius 1 (field of degree 5): rotating by μ = 0.01 gives cycles at radii 0.949 and 1.049; μ = −0.01 gives none.
• Two clocks at a saddle from height 10⁻⁶: time 13.8; exit heights 10⁻⁶, 0.25 and 0.87 for eigenvalues 1, 0.1 and 0.01.
• sin x = 0 on 0 < x < p: 3, 31 and 318 solutions for p = 10, 100 and 1000.

Read the source

• Uniform bounds for planar polynomial limit cycles (PDF), 160 pages.
• Two limit cycles for quintic Liénard systems (PDF), 40 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 143.

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

• Uniform bounds for planar polynomial limit cycles main paper
• Two limit cycles for quintic Liénard systems companion

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.