Papers With

← All papers
First page of Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach

Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach

Shangtong Zhang

cs.LG Nov 5, 2025 · v2 stat.ML
formalization mathlib probability ml-theory
Read PDF arXiv abstract Code
TL;DR
Formalizes almost sure convergence of Q-learning and linear TD with Markovian samples in Lean 4 using Mathlib, via the Robbins-Siegmund theorem.
Abstract
In this paper, we formalize the almost sure convergence of $Q$-learning and linear temporal difference (TD) learning with Markovian samples using the Lean 4 theorem prover based on the Mathlib library. $Q$-learning and linear TD are among the earliest and most influential reinforcement learning (RL) algorithms. The investigation of their convergence properties is not only a major research topic during the early development of the RL field but also receives significant attention nowadays. This paper formally verifies their almost sure convergence in a unified framework based on the Robbins-Siegmund theorem. The framework developed in this work can potentially be extended to convergence rates and other modes of convergence. This work thus makes an important step towards fully formalizing convergent RL results. The code is available at https://github.com/ShangtongZhang/rl-theory-in-lean.
Problem

Convergence proofs for reinforcement learning algorithms such as Q-learning and linear TD are delicate and error-prone; several published results have had documented gaps or errors. No machine-checked proofs of their almost sure convergence with Markovian samples existed.

Approach

The authors formalize finite Markov chains in Lean 4 with Mathlib: row-stochastic matrices, irreducibility, aperiodicity, Doeblin minorization, stationary distributions and geometric mixing. They build sample-path probability spaces from Mathlib probability kernels. Mathlib has little ODE theory, so they avoid the usual ODE-based approach. Instead, both algorithms are cast as stochastic approximation iterates and analyzed in a unified framework based on the Robbins-Siegmund theorem with Lyapunov functions.

Results

The work gives the first formal verification of almost sure convergence of linear TD and Q-learning with Markovian samples; the code is released publicly. The authors identify conditional expectation as the most technically challenging part. They outline extensions to convergence rates, concentration bounds and other TD methods.