Uniform Substitution for Differential Dynamic Logic in Lean

This repository contains a formalization of Differential Dynamic Logic (dL) in the Lean 4 proof assistant. It formalizes the syntax, static and dynamic semantics of dL, as well as Uniform Substitution, and includes proofs of the ODE axioms.

Contributors

• Oliver Enes
• Enguerrand Prebet