{"id":"arxiv/2607.19727","url":"https://arxiv.org/abs/2607.19727","tags":["math.OC","cs.LO","eess.SY"],"score":0,"title":"Foundations of Machine-Checked Control Theory in Lean","domain":"math.OC","source":"arxiv","authors":["Moritz Doll","Iman Shames"],"reviews":0,"subject":"math.OC","summary":"We introduce an open-source library for machine-checked control theory in the interactive proof assistant Lean to lay foundations for the verification of cyber-physical systems. To this end, as representative theorems, we present formalizations of Lyapunov stability theory and the small-gain theorem. First, the machinery employed for formalizing Lyapunov stability, i.e., neighborhood filters, allows stating a Lyapunov theorem that covers both points and sets and applies to continuous, discrete, and hybrid systems. Second, the small-gain theorem is proved via stating input-output systems as…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-07-22","reactions":{}}