---
id: "2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean"
url: "https://postcutoff.com/e/2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean/"
as_of: "2026-10-09T19:24:00+02:00"
date: "2026-10-08"
date_precision: day
category: science
importance: 3
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 3
editor: Adam Bicz
human_review: null
version: null
---

As of: 2026-10-09 19:24 CEST.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz.
Canonical page: https://postcutoff.com/e/2026-10-08-hilbert-number-lower-bound-gpt-5-6-sol-lean/

# 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

Full title: Hilbert's 16th problem: 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

On 8 Oct 2026 Chaoyang Qin and Xiaoming Sun (Institute of Computing Technology, CAS) posted arXiv 2610.12218, proving that the Hilbert number satisfies H(d) = Ω(d² ln² d), a factor ln d above the d² ln d bound that follows from Christopher–Lloyd (1995). The construction ("Hierarchical Melnikov Realization") perturbs an anisotropic Chebyshev Hamiltonian so that the first-order Melnikov function has simple zeros in many disjoint period annuli. "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 say the Lean 4 development has no unproved placeholders or project-specific axioms. They note that OpenAI's 6 Oct catalogue (family 143) claims the finiteness of H(d), the opposite, upper-bound side of the problem.

## 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

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 161 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 100 days after its cutoff
- Gemini 3.8 Flash (training cutoff March 2026): 191 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 130 days after its cutoff

## Sources

1. [Qin & Sun: Hierarchical Melnikov Realization: Logarithmic Factor Improvement to Hilbert Number Lower Bounds (arXiv 2610.12218)](https://arxiv.org/abs/2610.12218) (arxiv.org, paper)
2. [Lean formalization archive (Zenodo, doi:10.5281/zenodo.23219558)](https://doi.org/10.5281/zenodo.23219558) (doi.org, code)
3. [OpenAI math catalogue (CONTENTS.md, family 143)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, paper)

## Changes

- 2026-10-09 (filed): Created from the arXiv PDF

## Related

- 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)
- 2026-09-30: [Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help](https://postcutoff.com/e/2026-09-30-ai-assisted-conjecture-wave-summer-2026/index.md)