Publications

2025

1. PREPRINT

   A Formalization of the Ionescu-Tulcea Theorem in Mathlib

   Etienne Marion

   2025

   Abs arXiv

   We describe the formalization of the Ionescu-Tulcea theorem, showing the existence of a probability measure on the space of trajectories of a Markov chain, in the proof assistant Lean using the integrated library Mathlib. We first present a mathematical proof before exposing the difficulties which arise when trying to formalize it, and how they were overcome. We then build on this work to formalize the construction of the product of an arbitrary family of probability measures.

2. PREPRINT

   Formalization of Brownian motion in Lean

   Rémy Degenne, David Ledvinka, Etienne Marion, and Peter Pfaffelhuber

   2025

   Abs arXiv

   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éodory and Kolmogorov extension theorems, Gaussian measures in Banach spaces, and the Kolmogorov-Chentsov theorem for path continuity.