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

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.