Introduction: James Usevitch

Stream: new members

[James Usevitch]

Hi all, just wanted to introduce myself. James Usevitch, Assistant professor at BYU, background is in control theory and autonomous systems. Myself and one of my graduate students are interested in how Lean / Mathlib can be used to formalize theoretical results underpinning control theory, dynamical systems, and robotics.

What efforts are currently underway to apply or extend Mathlib to these areas? There seems to be a few components related to ODEs for Grönwall's inequality, Lipschitz continuity, and the Picard-Lindelöf theorem. There also appears to be a conversation from a few months back about formalizing Lyapunov stability, although it's unclear what came from that.

[Eric Wieser]

A slightly older thread that might be of interest

[James Usevitch]

@Eric Wieser Thanks for the link--that was helpful to read. Are you aware of whether any organized efforts came from this? It sounded like you had interest in this direction at the time.

[Eric Wieser]

I was never involved in any further organization, nor do I have much time to pursue the direction; but I remain interested!