The Lins-de Melo-Pugh conjecture for quintic Lienard systems: at most two limit cycles
Lins, de Melo and Pugh conjectured that the classical Lienard system , , with a real polynomial of degree , has at most limit cycles. The conjecture fails for every (Dumortier-Panazzolo-Roussarie in degree seven, De Maesschalck-Dumortier in degree six, De Maesschalck-Huzak in all degrees ) and holds for (Li and Llibre for the quartic case); Rychkov proved it for odd quintic . That left degree five. Does every classical Lienard system with have at most two limit cycles?
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Lienard systems; limit cycles
- Posed by
- A. Lins, W. de Melo and C. C. Pugh, On Lienard's equation (Lecture Notes in Mathematics 597, Springer, 1977)
- Year posed
- 1977
- Years open
- 49y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 25 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: if , with no parity or coefficient-sign assumption, the system , has at most two limit cycles in , counted as geometric images regardless of multiplicity, stability or hyperbolicity, and some member of the class has exactly two. This confirms the conjectured value . It concerns only the classical form with restoring force exactly ; generalized Lienard systems and other degrees are not treated. The paper also shows that a proposed degree-five four-cycle example of Hernandez Rosales has only two cycles.
What the AI did
The release README states that the vast majority of its results were produced by one fixed procedure with an unreleased internal OpenAI model, using on average about three hours of ChatGPT Pro thinking compute per result; roughly 4,000 problems were posed and the output was aggregated into result families and manuscripts, keeping those judged significant enough. This manuscript, dated September 24, 2026, is the companion in a two-manuscript family and comes with a Lean formalization in the release's lean/ library. The manuscript is credited to 'OpenAI' alone, names no human author and has no acknowledgements. The README's two exceptions to the fixed procedure (the zeta zero-free region work, whose Re(s) > 11/12 write-up was also human-edited, and the Hodge conjecture for CM abelian varieties) do not concern this family, so the result is presented as found and written up by the model. The release does not say how problems were chosen or how much human review happened before publication.
Verification
No independent mathematician has checked this yet. The release's formalization catalogue lists comparator config ComparatorChallenges/QuinticLienard.json with declaration OAI.QuinticLienard.main in OAI/Analysis/LienardCycles/Main.lean, permitted axioms propext, Quot.sound and Classical.choice. The comparator statement file was read: it defines the vector field (y - F(x), -x) for a real polynomial F, periodic orbits as ranges of nonconstant periodic solutions, and limit cycles as periodic orbits having an open neighbourhood that contains no other periodic orbit; it states that for deg F <= 5 the set of limit cycles has at most 2 elements and that some such F has exactly 2. That is the paper's headline claim, with no parity, sign or hyperbolicity assumption. Not rebuilt here: the Lean build and axiom check were not run. The paper's Theorem 1.1 was also read against the conjecture as quoted in its introduction.