Towards Formalizing Reinforcement Learning Theory
Shangtong Zhang
cs.LG
Nov 5, 2025 · v1
TL;DR
Formalizes almost-sure convergence of Q-learning and linear TD learning in the Lean 4 theorem prover atop the Mathlib library.
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 increasing 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 be easily 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
Q-learning and linear temporal difference (TD) learning are foundational reinforcement learning algorithms whose convergence proofs are mathematically involved. No prior formalization of their convergence existed in any proof assistant.
Approach
The authors formalize the almost sure convergence of Q-learning and linear TD learning with Markovian samples in Lean 4 using Mathlib. They employ the Robbins-Siegmund theorem as the proof foundation rather than ODE-based methods, since Mathlib lacks sufficient ODE infrastructure. The formalization defines stochastic vectors, row stochastic matrices, irreducibility, and aperiodicity, then establishes convergence within a unified framework applicable to both algorithms.
Results
This is the first formalization of the almost sure convergence of linear TD and Q-learning in any proof assistant. The developed framework is immediately applicable to formalizing additional convergent RL results, including L2 convergence rates with i.i.d. samples via conditional expectations and telescoping.
