Milan Korda

Lyapunov stability of polynomial vector fields is undecidable

We show that there are integers $N$ and odd $D$ such that no algorithm can decide, from the rational coefficients of a homogeneous polynomial vector field $F$ in dimension $N$ of degree $D$, whether the origin is Lyapunov stable for $\dot Y=F(Y)$. This proves a conjecture of V. I. Arnold. We provide a Lean formalizatio...