Proof-carrying nucleus-bottleneck Koopman autoencoders with Lean 4 verification, SafEDMD-inspired error bounds, and SDP Lyapunov controller synthesis for data-driven dynamical systems
dynamical-systems formal-verification mathlib controller-synthesis proof-carrying-code lyapunov-stability koopman-operator lean4 nucleus-bottleneck safedmd
-
Updated
Mar 20, 2026 - Lean