Abstract:

I will present a collaborative project in which we formalized the construction of Brownian motion in the Lean theorem prover. After an introduction to the probability theory part of Lean's mathematical library Mathlib, I will describe the Brownian motion project, its organization, and some of the formalized results. For that project, we developed the theory of Gaussian measures, 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. In a second part, I will discuss the ongoing next step of the project: formalizing stochastic integrals.

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk