Formalization of Brownian motion in the Lean theorem prover

I will present a collaborative project in which we formalized the construction of Brownian motion in Lean. Lean is an interactive theorem prover, with a large mathematical library called Mathlib. I will give an introduction to Lean and Mathlib, explain why one may want to formalize mathematics, and give a tour of the probability theory part of Mathlib. I will then describe the Brownian motion project, its organization, and some of the formalized results. For that project, we developed the theory of Gaussian measures and implemented a proof of Kolmogorov's extension theorem, as well as a modern version of the Kolmogorov-Chentsov continuity theorem based on Talagrand's chaining technique. Finally, I will discuss the next step of the project: formalizing stochastic integrals.