# Hilbert's sixteenth problem: uniform bounds for limit cycles

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Two limit cycles for quintic Liénard systems](../../preprints/two-limit-cycles-for-quintic-lienard-systems-September-24-2026/two-limit-cycles-for-quintic-lienard-systems-September-24-2026.pdf)

## Scope

For the quintic Liénard system $x'=y-F(x)$, $y'=-x$, the formalized result proves that every real polynomial $F$ of degree at most five yields at most two limit cycles, and that some such $F$ yields exactly two. Limit cycles are isolated images of nonconstant periodic solutions. No sign, parity, hyperbolicity, or amplitude restriction is imposed.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Exact two-cycle bound for quintic Liénard systems | [QuinticLienard.lean](../ComparatorChallenges/QuinticLienard.lean) |