How Deduction Systems Can Help You To Verify Stability Properties

Mathematical proofs are a cornerstone of control theory, and it is crucial to get them right. Deduction systems can help with this by mechanically checking the proofs. However, the structure and level of detail of mechanized proofs can differ vastly from manual proofs by mathematicians and engineers, hampering understanding and adoption of these systems.This paper helps bridging the gap between manual and machine-checked proofs by presenting a mechanized stability proof using Lyapunov’s theory in a human-readable way and wrapping it into a workflow. The proof structure is analyzed and potential benefits of mechanization are discussed, such as generalizability, reusability, and increased trust in correctness.