Qin & Sun prove H(d) = Ω(d² ln² d), the first log-factor gain since 1995, with GPT-5.6 Sol developing the proof and a Lean 4 certificate
Awaiting review
The takeaway
The lower bound for the number of limit cycles of degree-d planar polynomial vector fields improves from d² ln d to d² ln² d. The authors say GPT-5.6 Sol developed the proof strategy and arguments, and the construction is formalized in Lean 4.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 9 October 2026
Your AI and this story
- GPT-6 Astra161 days after its cutoff
- Claude Opus 5.5100 days after its cutoff
- Gemini 3.8 Flash191 days after its cutoff
- Grok 4.7130 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 100 days before it.
Key facts
- Main theorem: H(d) = Ω(d² ln² d) as d → ∞ (lower bound on the maximum number of limit cycles of real planar polynomial vector fields of degree d)
- Prior bounds: Otrokov 1954 (quadratic); Christopher & Lloyd 1995, order d² ln d along d = 2^k − 1, giving Ω(d² ln d) for all d; Li, Chan & Chung 2002 refined constants
- Method: anisotropic Chebyshev Hamiltonian, hierarchically chosen perturbation coefficients, two 3-adic filtrations for the log factors, and a Borel–Gauss analysis for the local rank condition
- Lean: the construction ‘is fully formalized in Lean 4’; the formal statements assert a degree-bounded polynomial vector field with an injective finite family of hyperbolic limit cycles; ‘no unproved placeholders or project-specific axioms’; code archived at Zenodo (doi:10.5281/zenodo.23219558)
- AI disclosure (verbatim): ‘GPT-5.6 Sol was used to develop the proof strategy and arguments throughout this paper, assist with Lean formalization, and edit the manuscript. The authors take full responsibility for the mathematical content and the final text.’
- Priority remark: ‘The main results were obtained by the end of August, at which time the finiteness of the Hilbert number H(d) remained an open problem’; OpenAI’s family 143 (dated 24 Sep, released 6 Oct) claims uniform finiteness, with only its quintic Liénard case in Lean
What happened
The second part of Hilbert’s 16th problem asks how many limit cycles a planar polynomial vector field of degree d can have. Upper bounds are out of reach, so most work builds systems with many cycles. The best growth rate, d² ln d, dates to Christopher and Lloyd in 1995. Qin and Sun gain another factor of ln d by placing simple zeros of the Melnikov function across many period annuli at once. They formalize the full construction in Lean 4.
Why it matters
It is a quantitative improvement on a 30-year-old bound for one of Hilbert’s problems, with a machine-checked construction and an AI model credited with developing the argument. It does not address finiteness, which OpenAI’s catalogue separately claims without a full formalization.
What is disputed or not yet verified
| Verification | Lean 4 formalization (per the authors); unrefereed preprint |
|---|
Sources
3 sources from 3 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
Changes
- Filed from the arXiv PDF