Lean 4 / Mathlib formalization of finite-N Kuramoto synchronization: ODE existence + uniqueness, order-parameter bounds, Lyapunov descent, and convergence to synchrony for all-to-all AND general symmetric coupling with a uniform positive off-diagonal floor. Sorry-free, axiom footprint {propext, Classical.choice, Quot.sound}.
synchronization theorem-proving dynamical-systems formal-verification hebbian-learning gradient-flow ai-safety lyapunov kuramoto-model mathlib max-cut lean4
-
Updated
Aug 25, 2026 - Lean