--- id: "2026-10-06-openai-hilbert-sixteenth-uniform-limit-cycle-bound-claim" url: "https://postcutoff.com/e/2026-10-06-openai-hilbert-sixteenth-uniform-limit-cycle-bound-claim/" as_of: "2026-10-30T13:42:00+01:00" date: "2026-10-06" date_precision: day category: science importance: 5 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 8 editor: human editor human_review: null version: "2026-10-29" --- As of: 2026-10-30 13:42 CET. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-10-06-openai-hilbert-sixteenth-uniform-limit-cycle-bound-claim/ # Hilbert's 16th problem: uniform limit-cycle bound claimed (OpenAI) Full title: OpenAI's math release claims the uniform-boundedness part of Hilbert's sixteenth problem (the number of limit cycles of a planar polynomial vector field is bounded in terms of its degree); only a quintic Liénard companion is in Lean Family 143 of OpenAI's 6 Oct 2026 math release, "Uniform bounds for planar polynomial limit cycles" (OpenAI, 24 Sept, 160 pages), claims: "For every degree, we prove that the number of isolated periodic orbits of a real planar polynomial vector field is bounded by a finite constant depending only on that degree. This establishes the uniform boundedness assertion in the second part of Hilbert's sixteenth problem." The constant B(d) is not effective. The only Lean statement in the family is a companion theorem: every classical Liénard system with polynomial F of degree at most five has at most two limit cycles, and two occur (the degree-five case of the Lins Neto–de Melo–Pugh conjecture); it was accepted in the community comparator run. Carlos Toledo's audit lists the uniform bound first among headlines "carried by no machine-checked statement". No expert reaction found. ## Key facts - Main manuscript: 'Uniform bounds for planar polynomial limit cycles' (OpenAI, 24 Sept 2026, 160 pages). Theorem 1.1 (verbatim): 'For each integer d ≥ 1, there is a finite nonnegative 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.' The paper adds: 'It does not furnish an effective formula for B(d).' Method (abstract): 'separation of asymptotic expansions on nested complex domains and a finite-dimensional counting argument' - Background as the paper recounts it: Dulac claimed individual finiteness (each fixed field has finitely many limit cycles) in 1923; after a gap was found, Écalle and Ilyashenko gave proofs; uniform boundedness (a bound depending only on the degree) stayed open, with partial results such as Bautin's bound of three for quadratic weak foci, finite cyclicity of elementary polycycles (Ilyashenko–Yakovenko) and explicit bounds for zeros of Abelian integrals (Binyamini–Novikov–Yakovenko). Wikipedia: no upper bound is known for any degree n > 1 - Companion manuscript: 'Two limit cycles for quintic Liénard systems' (24 Sept, 40 pages): every system ẋ = y − F(x), ẏ = −x with real polynomial F 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.' Lean scope note (lean/docs/143.md): challenge QuinticLienard, no sign, parity, hyperbolicity or amplitude restriction; 'accepted' in the oai-math-revised comparator run of 25–26 Oct - Carlos Toledo's audit of the release (cert-machine, finding G1, 10 Oct): 'Of the release's 416 statements, only QuinticLienard defines periodic orbits or limit cycles at all'; the uniform-bound manuscript 'is not linked by the scope note', whose title nevertheless names the uniform bounds. He lists Hilbert's sixteenth problem first among five headlines 'carried by no machine-checked statement' - Related human work: Chaoyang Qin and Xiaoming Sun's lower bound H(d) = Ω(d² log² d) (arXiv 2610.12218, 8 Oct, obtained with GPT-5.6 Sol and formalized in Lean) is complementary; they write that when their results were obtained in August 'the finiteness of the Hilbert number H(d) remained an open problem' (see [2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean](https://postcutoff.com/e/2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean/index.md)) - Reactions: Alvaro Lozano-Robledo listed 'the second part of Hilbert’s 16th' among proposed solutions that 'would represent huge contributions to their respective fields' (Proofs and Prompts, 8 Oct). No assessment by a specialist in planar dynamics or limit cycles found (web, Hacker News, oai-math-revised notes) as of 29 Oct ## What happened A limit cycle is an isolated periodic orbit of a planar vector field. The second part of Hilbert's sixteenth problem asks how many limit cycles a polynomial field of degree d can have. Two questions are mixed in it. Individual finiteness says each fixed field has finitely many; it was proved by Écalle and by Ilyashenko after Dulac's 1923 argument turned out to have a gap. Uniform boundedness asks for a bound depending only on d. It had not been proved for any degree above one. OpenAI's 6 Oct release includes a 160-page manuscript, dated 24 Sept, that claims uniform boundedness for every degree, with a bound it does not compute. A second manuscript treats a special case exactly: quintic Liénard systems have at most two limit cycles. Only that special case is formalized in Lean, and a community comparator run accepted it. An independent audit pointed out that the family's title promises the uniform bound while no Lean statement in the release even defines limit cycles for general polynomial fields. ## Why it matters If correct, the result answers the existence half of one of Hilbert's problems, though not the question of how large B(d) is. Here the Lean label applies only to the special case, so the main claim rests on the manuscript alone. A month after the release no specialist has said in public whether the argument holds. It is among the most famous claims in the release that our coverage had listed only in passing. ## What is disputed or not yet verified - Verification: Main claim: unrefereed 160-page manuscript, not formalized; only the quintic Liénard companion is Lean-formalized (comparator-accepted) ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff - Grok 4.7 (training cutoff May 2026): 128 days after its cutoff ## Sources 1. [OpenAI (PDF): Uniform bounds for planar polynomial limit cycles (24 Sept 2026)](https://github.com/openai/math/blob/main/preprints/uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026/uniform-bounds-for-planar-polynomial-limit-cycles-September-24-2026.pdf) (github.com, paper) 2. [OpenAI (PDF): Two limit cycles for quintic Liénard systems (24 Sept 2026)](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) (github.com, paper) 3. [OpenAI Lean scope note for family 143 (quintic Liénard only)](https://github.com/openai/math/blob/main/lean/docs/143.md) (github.com, code) 4. [oai-math-revised comparator results (QuinticLienard accepted)](https://github.com/mathcommunity/oai-math-revised/blob/main/checks/comparator-2026-10-26/results.tsv) (github.com, code) 5. [arXiv 2610.12218: Qin & Sun, Hilbert number lower bound Ω(d² log² d)](https://arxiv.org/abs/2610.12218) (arxiv.org, paper) 6. [Wikipedia: Hilbert's sixteenth problem](https://en.wikipedia.org/wiki/Hilbert%27s_sixteenth_problem) (en.wikipedia.org, docs) 7. [Carlos Toledo: OpenAI's math release, what it claims beyond what it checks (finding G1)](https://carlostoledo.co/reports/openai-math.html) (carlostoledo.co, discussion) 8. [Proofs and Prompts: 100+ reactions to 100+ solutions (8 Oct)](https://proofsandprompts.com/2026/10/08/100-reactions-to-100-solutions/) (proofsandprompts.com, discussion) ## Changes - 2026-10-29 (filed): Created (CONTENTS entry, both PDFs (160 and 40 pp), Lean scope note, comparator results, Qin–Sun entry, Proofs and Prompts reactions; web and HN searches found no specialist comment) ## Related - 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md) - 2026-10-08: [Hilbert's 16th problem](https://postcutoff.com/e/2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean/index.md) - 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)