# A Formalization of the Ionescu-Tulcea Theorem in Mathlib

arXiv: https://arxiv.org/abs/2506.18616 · HTML: https://mlsanity.com/paper/2506.18616/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Jun 2025.

## Built on by (most cited first, 2 of 2)

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean](https://mlsanity.com/paper/2609.09264/) (2026)

## Abstract (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.