Integral Curves and Flows on Banach Manifolds in Lean

TL;DR

This paper formalizes key theorems about integral curves of vector fields on Banach manifolds within the Lean theorem prover, establishing a foundation for future work in dynamical systems and differential geometry.

Contribution

It introduces a formalization of existence and uniqueness theorems for integral curves on Banach manifolds in Lean, extending differential equations results to abstract manifolds.

Findings

Formalization of Picard-Lindelöf theorem in Lean

Transfer of differential equations results to Banach manifolds

Foundation for future dynamical systems libraries

Abstract

We present a formalisation of the existence and uniqueness theorems of integral curves of vector fields on Banach manifolds in the Lean theorem prover. First, we formalize properties of differential equations on Banach spaces (the Picard-Lindel\"of theorem, the Gr\"onwall inequality, and corollaries), and then transfer results to abstract Banach manifolds. Built upon the differential and integral calculus and Banach manifolds libraries in Mathlib, our work aims to lay the foundation for dynamical systems and differential geometry libraries that are general, robust, and friendly to classical mathematicians.