Formalization of Brownian motion in Lean
Probability
2025-12-03 v2
Abstract
Brownian motion is a building block in modern probability theory. In this paper, we describe a formalization of Brownian motion using the Lean theorem prover. We build on the existing measure-theoretic foundations in Lean's mathematical library, Mathlib, and we develop several key components needed for the construction of Brownian motion, including the Carath\'eodory and Kolmogorov extension theorems, Gaussian measures in Banach spaces, and the Kolmogorov-Chentsov theorem for path continuity.
Keywords
Cite
@article{arxiv.2511.20118,
title = {Formalization of Brownian motion in Lean},
author = {Rémy Degenne and David Ledvinka and Etienne Marion and Peter Pfaffelhuber},
journal= {arXiv preprint arXiv:2511.20118},
year = {2025}
}