Brownian motion is a foundational object in modern probability theory, but it had not been formally constructed in the Lean theorem prover. The construction requires several deep theorems not previously available in Mathlib.

The authors formalize Brownian motion in Lean, building on Mathlib's measure-theoretic foundations. They develop key components including the Caratheodory and Kolmogorov extension theorems, Gaussian measures in Banach spaces, and the Kolmogorov-Chentsov theorem for path continuity.

A stochastic process with continuous paths, starting at zero, and with Gaussian increments is constructed in Lean. The formalization contributes new infrastructure for random variables and stochastic processes to Mathlib, including probability distributions, characteristic functions, and path regularity results.