Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Conjecture 2: Ha(2)=1H_a(2)=1Ha​(2)=1

Open
HilbertSixteenth.quadratic_algebraic_conjecture

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

dynamical-systemshilbert-16th-problemlimit-cycles

Every quadratic polynomial vector field (degree at most 222) has at most one algebraic limit cycle, and some quadratic vector field has exactly one:

Ha(2)=1.H_a(2)=1.Ha​(2)=1.

This is the simplest case of Conjecture 1 and is open.

Preamble
import Definitions.Def_HilbertSixteenth_PolyFields
Formal statement
namespace HilbertSixteenth
theorem quadratic_algebraic_conjecture : algebraicHilbertNumber 2 = 1 := 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 2.
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.

The algebraic Hilbert number at d=2d=2d=2 equals 111: the supremum, over all polynomial vector fields V=(P,Q)V=(P,Q)V=(P,Q) with max⁡(totdeg⁡P,totdeg⁡Q)≤2\max(\operatorname{totdeg}P,\operatorname{totdeg}Q)\le2max(totdegP,totdegQ)≤2, of the number (in N∪{∞}\mathbb N\cup\{\infty\}N∪{∞}) of algebraic limit cycles of VVV (limit cycles contained in the real zero set of a non-zero polynomial) is exactly 111. Equivalently: every such VVV has at most one algebraic limit cycle, and at least one such VVV has exactly one.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me