Formalization of the Ionescu-Tulcea theorem in Mathlib

Abstract: 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 Markov kernels, which are the objects of interest in this theorem. Then after giving a glimpse of the proof, we expose the difficulties which arise when trying to formalize it, and how they were overcome.

mathematical softwareprobability

Audience: advanced learners

( paper | slides | video )

Lean Together 2026