Integral Curves and Flows on Banach Manifolds in Lean
Differential Geometry
2026-02-17 v1
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.
Cite
@article{arxiv.2602.13247,
title = {Integral Curves and Flows on Banach Manifolds in Lean},
author = {Weichen Winston Yin and Yury Kudryashov},
journal= {arXiv preprint arXiv:2602.13247},
year = {2026}
}