Verified Koopman: SafEDMD Extension
Formal Verification Certificate
Every theorem in this project has been machine-checked by the Lean 4 kernel. No axiom is assumed without proof. No gap exists in the verification chain.
Verified Koopman: SafEDMD Extension • Lean 4 + Mathlib • Apoth3osis Labs
SafEDMD-Inspired Error Bounds
This project extends the Nucleus Bottleneck Autoencoder with SafEDMD-inspired residual-covariance error bounds, SDP Lyapunov controller synthesis, and a Platinum verification tier. Building on Strässer, Berberich & Allgöwer's data-driven control framework, we provide machine-checked guarantees that the nucleus bottleneck preserves energy bounds, Heyting lattice structure, and Gram matrix constraints throughout the Koopman pipeline.
- • 10 sorry-free Lean 4 modules with 41 theorems
- • SafEDMD energy bound:
Σ R(v)² ≤ Σ v² - • Heyting adjunction for both fixed and learned bounds
- • 4 corrections/extensions vs the original paper
Nucleus Bottleneck Autoencoder
This extension builds on the original NBA, which constrains Koopman autoencoder latent space to a Heyting-algebra-valued slice governed by nucleus maps. The verified-koopman repo adds SafEDMD-style error guarantees on top of those foundational proofs.
Strässer, Berberich & Allgöwer developed the SafEDMD framework for data-driven control with guaranteed error bounds. Our formalization extends their algebraic ingredients with nucleus-aware Heyting structure and machine-checked proofs.
Robin Strässer
Research Associate · Control Systems
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Research associate at IST Stuttgart working on data-driven control methods for nonlinear systems. Lead author of the SafEDMD framework (Automatica 2027) which provides guaranteed error bounds for Extended Dynamic Mode Decomposition with noisy measurement data.
Julian Berberich
Researcher · Data-Driven Control
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Researcher at IST Stuttgart specializing in data-driven control theory with rigorous guarantees. Co-author of the SafEDMD framework and fundamental data-driven representations for control.
Frank Allgöwer
Professor · Director of IST
Institute for Systems Theory and Automatic Control (IST), University of Stuttgart
Full professor and director of IST Stuttgart. One of the most-cited researchers in control theory worldwide. ERC Advanced Grant recipient (2016). Research spans nonlinear control, model predictive control, and systems biology.
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.