Hilberts 16th Problem

### What is the conjecture

Hilbert's sixteenth problem consists of two related questions about real algebraic geometry and polynomial dynamical systems:

**Part 1 (Real Algebraic Curves):** For a real algebraic plane curve of degree $n$ defined by a polynomial $f(x, y) \in \mathbb{R}[x, y]$, the connected components are called *ovals*. The problem asks to:
- Classify all possible topologies of the ovals (their relative positions and enclosures)
- Determine the maximum number of ovals, bounded by Harnack's theorem: at most $(n-1)(n-2)/2 + 1$ ovals

**Part 2 (Limit Cycles):** For a planar polynomial vector field $\dot{x} = P(x, y)$, $\dot{y} = Q(x, y)$ with $\deg(P), \deg(Q) \leq n$, determine:
- Whether there exists a finite bound $H(n)$ on the maximum number of isolated closed trajectories (limit cycles)
- If so, find explicit bounds or formulas for $H(n)$

The first part has been fully resolved through isotopy classification (completed for degrees up to 8). The second part remains open for any $n > 1$, though it is known that $H(n)$ must grow at least as fast as $n^2 \log n$.

**Sources:**
- https://en.wikipedia.org/wiki/Hilbert's_sixteenth_problem, https://www.ams.org/journals/bull/2002-39-03/S0273-0979-02-00946-1/S0273-0979-02-00946-1.pdf, https://www.birs.ca/workshops/2007/07w5021/report07w5021.pdf, https://arxiv.org/abs/2411.09594, https://link.springer.com/article/10.1007/s11537-008-0832-6

### Prerequisites needed

**Formalizability Rating:** 5/5 (0 is best) (as of 2026-01-20)

Mathlib provides foundational support for polynomials, algebraic varieties, and basic topology. However, formalizing Hilbert's 16th problem requires significant new infrastructure: (1) Real algebraic geometry with emphasis on real points and real topology of algebraic varieties; (2) Topological classification of real curves and ovals; (3) Rigorous treatment of polynomial vector fields and limit cycles as dynamical objects; (4) Harnack's bound and related results in real algebraic geometry. These represent substantial theory development beyond current Mathlib coverage, warranting a rating of 5.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-14
* ams-37
* ams-12

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me, again I am not a 100% if the statement is correct as is but the sources look good.

Start by checking the cited sources and the repository's conventions for adding formal conjecture statements; no specific files or tests are named in the issue. Clarify which part of the problem is intended and establish a precise formal statement before implementation, with completion requiring an accepted formalization and suitable verification.

Written by the indexing model from the issue text.