Conjecture 1: $H_a(d)=1+\frac{(d-1)(d-2)}{2}$

Open

HilbertSixteenth.llibre_conjecture

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemshilbert-16th-problemlimit-cycles

For every $d\ge2$ , the algebraic Hilbert number — the supremum over all planar polynomial vector fields of degree at most $d$ of the number of their algebraic limit cycles — equals

H_a(d)=1+\frac{(d-1)(d-2)}{2}.

That is, every polynomial differential system of degree at most $d$ has at most $1+\frac{(d-1)(d-2)}2$ algebraic limit cycles, and some system of degree at most $d$ has exactly that many.

This is the conjectured answer to Problems 6 and 7 of the survey: a uniform bound for the number of algebraic limit cycles depending only on the degree, together with its sharp value.

Formalization Note The count and the supremum are taken in ℕ∞, so the statement also asserts that the supremum is finite. The source asserts the conjecture without an explicit range of $d$ ; $d\ge2$ is imposed because for $d=1$ the right-hand side is $1$ while linear systems have no limit cycles.

Preamble

import Definitions.Def_HilbertSixteenth_PolyFields

Formal statement

namespace HilbertSixteenth
theorem llibre_conjecture (d : ℕ) (hd : 2 ≤ d) :
    algebraicHilbertNumber d = ((1 + (d - 1) * (d - 2) / 2 : ℕ) : ℕ∞) := by sorry
end HilbertSixteenth

Source

J. Llibre, *Sobre el problema 16 de Hilbert*, La Gaceta de la RSME 18 (2015), no. 3, pp. 543–554, §7, Conjecture 1 (first stated in Llibre–Ramírez–Sadovskaia, J. Differential Equations 248 (2010) 1401–1409).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, at the explicit request of the proposal owner. It is not independent testimony: its author knew the intended meaning of the code while writing it, so it may unconsciously read that intent into the code. Reviewers should compare the Lean code against the source directly and should not treat this text as an independent audit.

For every natural number $d\ge2$ :

H_a(d)=1+\frac{(d-1)(d-2)}{2},

where the right-hand side is computed in $\mathbb N$ (truncated subtraction and floor division; for $d\ge2$ the product is even so the division is exact) and cast to $\mathbb N\cup\{\infty\}$ , and $H_a(d)$ is the supremum in $\mathbb N\cup\{\infty\}$ , over all polynomial vector fields $V=(P,Q)$ with $\max(\operatorname{totdeg}P,\operatorname{totdeg}Q)\le d$ , of the cardinality in $\mathbb N\cup\{\infty\}$ of the set of algebraic limit cycles of $V$ . An algebraic limit cycle of $V$ is a set that is the image of a global non-constant periodic solution of $\gamma'=V(\gamma)$ , has an open neighbourhood $U$ such that no other periodic orbit of $V$ is contained in $U$ , and lies in the real zero set of some non-zero polynomial (of any degree). The equality asserts both that no such $V$ has more than $1+(d-1)(d-2)/2$ algebraic limit cycles and that the supremum is attained or approached — since the values are natural numbers, some $V$ attains it. For $d=2$ the value is $1$ , for $d=3$ it is $2$ , for $d=4$ it is $4$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Conjecture 1: Ha(d)=1+(d−1)(d−2)2H_a(d)=1+\frac{(d-1)(d-2)}{2}Ha​(d)=1+2(d−1)(d−2)​

Conjecture 1: $H_a(d)=1+\frac{(d-1)(d-2)}{2}$