Papers With

← All papers
First page of Integral Curves and Flows on Banach Manifolds in Lean

Integral Curves and Flows on Banach Manifolds in Lean

Weichen Winston Yin, Yury Kudryashov

math.DG Feb 2, 2026 · v1
formalization mathlib analysis
Read PDF arXiv abstract
TL;DR
Formalizes existence and uniqueness of integral curves of vector fields on Banach manifolds in Lean atop Mathlib.
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öf theorem, the Grönwall 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.
Problem

The existence and uniqueness theorems for integral curves and flows of vector fields on Banach manifolds lack formalization in proof assistants, limiting the foundation for mechanized dynamical systems and differential geometry.

Approach

The authors formalize in Lean properties of differential equations on Banach spaces (the Picard-Lindelof theorem, the Gronwall inequality, and corollaries) and then transfer these results to abstract Banach manifolds. The work builds on Mathlib libraries for differential and integral calculus and Banach manifolds, establishing infrastructure for dynamical systems formalization.

Results

The formalization covers existence, uniqueness, and smooth dependence on initial conditions for integral curves on Banach manifolds, laying foundations for dynamical systems and differential geometry libraries in Lean that are general and compatible with classical mathematical conventions.