Uniform bounds for limit cycles in Hilbert's sixteenth problem

The second part of Hilbert's sixteenth problem asks for the maximum number and arrangement of limit cycles of real planar polynomial vector fields. Its uniform boundedness assertion asks whether the number of limit cycles is bounded by a constant depending only on the degree. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), both dated 24 September 2026, make claims on this question. The first claims uniform boundedness in every degree. The second claims that classical Liénard systems with a polynomial of degree at most five have at most two limit cycles, which is the degree-five case of the Lins Neto–de Melo–Pugh conjecture. This page summarizes the published claims and lists publicly available follow-up work.

Background

• Limit cycles. Both manuscripts call a periodic orbit a limit cycle if some open neighbourhood of it contains no other periodic orbit, and count each orbit once.
• As recounted in the introduction of the uniform-bounds manuscript:
  • Individual finiteness (for one fixed vector field) differs from uniform boundedness (a bound depending only on the degree). Finiteness for every member of a family does not by itself bound the numbers as the coefficients vary.
  • Dulac claimed individual finiteness in 1923. After a gap in that argument was identified, Écalle and Ilyashenko gave proofs using complex and asymptotic analysis of return maps.
  • Yeung identifies a coefficient-closure obstruction in a leading-term argument of Ilyashenko's 1991 monograph. The manuscript notes that this concerns that proof mechanism and is not a counterexample to individual finiteness.
  • Partial uniform results include:
    • Bautin's sharp bound of three for cycles bifurcating from a weak focus or centre of a quadratic field;
    • finite cyclicity of elementary polycycles in generic families (Ilyashenko and Yakovenko), with an explicit bound by Kaloshin;
    • explicit bounds for the infinitesimal problem (Binyamini, Novikov and Yakovenko);
    • o-minimal and quasianalytic approaches (Kaiser, Rolin and Speissegger; Galal, Kaiser and Speissegger).
• As recounted in the introduction of the Liénard manuscript, for the classical Liénard system ẋ = y − F(x), ẏ = −x:
  • The conjecture. Lins Neto, de Melo and Pugh (1977) conjectured the bound ⌊(n − 1)/2⌋ when deg F = n.
  • Known cases. Rychkov proved the two-cycle bound for odd quintic F. Li and Llibre proved the bound of one cycle in degree four.
  • Counterexamples. Dumortier, Panazzolo and Roussarie found four cycles in degree seven, and De Maesschalck and Dumortier found four in degree six. De Maesschalck and Huzak constructed at least n − 2 cycles in every degree n ≥ 6.
  • Degree five. These results left degree five undecided. The manuscript cites a preprint of Chen, Li, Zhang and Zhang (arXiv:2608.19542v1, August 2026), which reports the unrestricted quintic problem as open. In degree five, Li and Lu had bounded by two the cyclicity of nondegenerate slow–fast cycles, a bound in a limiting regime.

The original results

• Uniform boundedness (24 September 2026). Theorem: for each integer d ≥ 1 there is a finite integer 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. There is no restriction on the coefficients, the locations of the cycles or their stability. The manuscript states that it gives no effective formula for B(d).
• Method, as described in that manuscript.
  • A return is represented by equations matching the endpoints of finitely many local passages, with cuts allowed to move along the orbit. The manuscript names Ilyashenko and Yakovenko's cyclic systems as a predecessor.
  • The proof uses separation of asymptotic expansions on nested complex domains (Section 3), differentiated implicit closure and elimination, and a finite-dimensional counting argument (Section 11).
  • It does not use individual finiteness as a premise.
• Quintic Liénard systems (24 September 2026). Theorem 1.1: if deg F ≤ 5, the system ẋ = y − F(x), ẏ = −x has at most two limit cycles in the plane, and some members of the class have two. No parity or coefficient-sign assumption is imposed on F.
  • Method, as described: the two half-orbits are treated separately. In the coordinate u = x²/2 they are compared with quadratic profiles through a global interpolation theorem. A separate section proves the lower bound.
  • A comment on another preprint: the manuscript argues that a degree-five example proposed by Hernández Rosales (2026 preprint, Section 9) as having four cycles is Odani's Example 3 after a change of variable, and so has exactly two.
• Sources. Commit 1581d4c of the openai/math repository:
  • Uniform bounds for planar polynomial limit cycles;
  • Two limit cycles for quintic Liénard systems.
• Formalization, as described by the repository.
  • The scope note lean/docs/143.md links only the Liénard manuscript. It states that the formalization proves the bound of two limit cycles for every real F of degree at most five, attained for some F, with no sign, parity, hyperbolicity or amplitude restriction.
  • The Comparator challenge QuinticLienard.lean states main. Every real polynomial F with degree at most 5 has at most two limit cycles, and some such F has exactly two. A limit cycle is defined there as the range of a nonconstant periodic solution with an open neighbourhood containing no other periodic orbit.
  • The uniform boundedness theorem is not among the selected statements.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial": only the quintic Liénard system is stated (at most two limit cycles, exactly two attained), and the general uniform boundedness theorem is not. Records a sandboxed Comparator pass for QuinticLienard.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list QuinticLienard. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the QuinticLienard solution (1,061 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-08	C. Qin and X. Sun, arXiv:2610.12218v1, Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds	Remark (complementary result)	Proves the lower bound H(d) = Ω(d2 ln2 d) for the Hilbert number, improving the previously known lower bound by a factor of ln d. The construction perturbs an anisotropic Chebyshev Hamiltonian, and the abstract states that it is formally certified in Lean 4 (the paper links the repository AscendFoam/hierarchical-melnikov-lean). A closing remark states that the main results were obtained by the end of August, when finiteness of H(d) was open. It notes that an OpenAI draft claiming a proof of finiteness was released on 6 October 2026, and that its lower bounds are independent of that draft.	arXiv preprint (v1).
2026-10-09	H. Chen, L. Chen and Y. Xiao, arXiv:2610.13080v1, Limit cycles of slow-fast quintic Lienard systems	Related (special regime)	For every fixed real quintic F, the slow–fast system ẋ = y − F(x), ẏ = −εx has at most two limit cycles for 0 < ε < ε0(F). The bound is sharp, for F = 3x5 − 50x3 + 135x. The paper notes that by rescaling, for any fixed ε > 0, the supremum over deg F = n is the classical maximum L(n). It conjectures that L(n) is attained in the slow–fast regime for n ≥ 6. Version 1 does not refer to the openai/math manuscripts.	arXiv preprint (v1).

Notes

• The kernel checks above concern the formal statement QuinticLienard.main as written. The uniform boundedness theorem has no formal statement in the collection.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.