Browse › Dynamical systems and ergodic theory › 143 Hilbert's sixteenth problem: uniform bounds for limit cycles
Two limit cycles for quintic Liénard systems
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Hilbert's sixteenth problem: uniform bounds for limit cycles — Lean scope notes (lean/docs/143.md, release of 6 October 2026). States that the formalization proves Theorem 1.1 (at most two limit cycles for every real F with deg F ≤ 5, and exactly two for some F), with no sign, parity, hyperbolicity or amplitude restriction; it does not cover the companion manuscript's uniform bound for arbitrary planar polynomial vector fields. [family-level]
- OpenAI math release, QuinticLienard.lean (comparator statement) (lean/ComparatorChallenges/QuinticLienard.lean). The standalone statement of the two-part theorem (encard ≤ 2 for all F of degree ≤ 5; encard = 2 for some F), with the proof left as
sorryas a comparator target. - OpenAI math release, OAI.QuinticLienard.main (lean/OAI/Analysis/LienardCycles/Main.lean). The release's proof of the main theorem, assembled from
upper_boundandSharpness.sharpnessin the same development.
Possibly relevant literature (found by the agent, not checked)
- Hebai Chen, Leshan Chen and Yu Xiao, Limit cycles of slow-fast quintic Lienard systems (arXiv:2610.13080, 9 October 2026). Independently proves that for each fixed real quintic F, $\dot x=y-F(x)$, $\dot y=-\varepsilon x$ has at most two limit cycles for small ε > 0, with a two-cycle example; it covers the slow–fast regime of Theorem 1.1, presents itself as complementing Li–Lu, and does not mention the release.
- Chen Cao, Nasrin Sadri, Yilei Tang and Zhaoxia Wang, Global Dynamics and Periodic-Annulus Bifurcations in a Reversible Quintic Liénard System (arXiv:2610.26699, 19 October 2026). A study of a different (reversible) quintic Liénard family whose introduction states that the maximum number of limit cycles of a general classical quintic Liénard equation "is still unknown"; it does not mention the release.
- Valery A. Gaiko, Liénard's system and Smale's problem (arXiv:math/0611143, November 2006). An earlier preprint claiming a solution of Smale's thirteenth problem on the maximum number of limit cycles of Liénard polynomial systems, by field-rotation methods; relevant as prior claimed work on the bound addressed in Theorem 1.1.
Digests and expositions
- Singh-AP, ai-math-papers-explained: Uniform bounds for planar polynomial limit cycles (GitHub, accessed 2026-10-21). A beginner-level explainer filed under the uniform-bounds paper that also covers this companion's theorem, proof outline, a two-cycle example and its Lean formalization; the README states that the slides, infographics, report and audio were generated with NotebookLM. [AI-generated per source] [family-level]
News and blogs
- Azmat, Hilbert's 16th Problem: OpenAI's Limit-Cycle Proof Explained (Binary Verse AI, 10 October 2026). A blog explainer of the family that describes this paper's result as covering a restricted family with at most two limit cycles; it quotes no outside experts. [family-level]
- Carlos Toledo, OpenAI's math release: what it claims beyond what it checks (self-published audit, findings dated 10 October 2026). Finding G1 distinguishes the family's general uniform-bound claim from the quintic Liénard theorem covered by its Lean statements at the audited commit
fd4aeeb2. [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 143
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/143.md. The Lean statements have not been checked by people against the paper's claims.
Family 143: 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.
Other papers in this family:
- Uniform bounds for planar polynomial limit cycles · September 24, 2026