Papers With

← All papers
First page of A Globally Asymptotically Stable Planar Homogeneous Polynomial Vector Field With No Polynomial Lyapunov Function

A Globally Asymptotically Stable Planar Homogeneous Polynomial Vector Field With No Polynomial Lyapunov Function

Jun Liu, Maxwell Fitzsimmons

math.DS Jul 17, 2026 · v1 eess.SY math.OC
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Provides a machine-checked Lean 4 formalization of the main result disproving the homogeneous polynomial Lyapunov converse conjecture.
Abstract
We disprove the conjecture that every globally asymptotically stable homogeneous polynomial vector field admits a homogeneous polynomial Lyapunov function. The counterexample is a planar homogeneous cubic polynomial vector field with integer coefficients. It admits no positive definite homogeneous polynomial with nonpositive Lie derivative and, more strongly, no real-analytic Lyapunov function even locally. Nevertheless, it has an explicit degree-two homogeneous Lyapunov function that is radially unbounded, continuously differentiable everywhere, and smooth away from the origin. We also provide a machine-checked Lean 4 formalization of the main result.
Problem

It was conjectured that every globally asymptotically stable homogeneous polynomial vector field admits a homogeneous polynomial Lyapunov function. Whether this conjecture holds was open and connected to decidability of stability for polynomial vector fields.

Approach

A planar homogeneous cubic vector field with integer coefficients is constructed as a counterexample. Polar coordinates are used to derive the dynamics and verify an explicit degree-two exponential Lyapunov function. Fourier-mode and leading-term arguments exclude any homogeneous polynomial or local real-analytic Lyapunov function. The main result is formalized in Lean 4.

Results

The system is globally asymptotically stable with an explicit C^1, smooth-away-from-origin Lyapunov function, yet admits no positive definite homogeneous polynomial with nonpositive Lie derivative and no local real-analytic Lyapunov function, disproving the conjecture.