`lyapunov-odes-lean` is a Lean 4 / Mathlib library formalising core Lyapunov stability theorems for autonomous ordinary differential equations. The library defines solutions of `x' = f(x)` using `HasDerivAt`, states Lyapunov stability and asymptotic stability at the origin, proves a Lyapunov stability theorem, proves an asymptotic-stability theorem with the LaSalle convergence step factored into an explicit hypothesis, and proves exponential decay through Mathlib's Gronwall inequality. The development contains zero `sorry`, zero `admit`, and uses standard Lean/Mathlib axioms only. It provides a checked stability-theory component for later work on control, dynamical systems, optimisation dynamics, and AI safety.