# Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach arXiv: https://arxiv.org/abs/2511.03618 ยท HTML: https://mlsanity.com/paper/2511.03618/ ## Key facts - Cited by 7 papers in the map (data through 14 Oct 2026). - Placed in RL theory and sample complexity, one of 15 directions in Deep reinforcement learning methods. - Builds on 37 of its 82 references that are in the map. - First posted on arXiv 5 Nov 2025. ## Placed in - Deep reinforcement learning methods / [RL theory and sample complexity](https://mlsanity.com/deeprl/rl-theory-and-sample-complexity/) ## Builds on (most cited first, 30 of 37) - [On the Global Convergence Rates of Softmax Policy Gradient Methods](https://mlsanity.com/paper/2005.06392/) (2020) - [A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation](https://mlsanity.com/paper/1806.02450/) (2018) - [On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift](https://mlsanity.com/paper/1908.00261/) (2019) - [Finite-Time Error Bounds For Linear Stochastic Approximation and TD Learning](https://mlsanity.com/paper/1902.00923/) (2019) - [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019) - [An Emphatic Approach to the Problem of Off-policy Temporal-Difference Learning](https://mlsanity.com/paper/1503.04269/) (2015) - [Finite-Time Analysis of Asynchronous Stochastic Approximation and Q-Learning](https://mlsanity.com/paper/2002.00260/) (2020) - [Sample Complexity of Asynchronous Q-Learning: Sharper Analysis and Variance Reduction](https://mlsanity.com/paper/2006.03041/) (2020) - [Is Q-Learning Minimax Optimal? A Tight Sample Complexity Analysis](https://mlsanity.com/paper/2102.06548/) (2021) - [Finite-Sample Analysis for SARSA with Linear Function Approximation](https://mlsanity.com/paper/1902.02234/) (2019) - [Learning and Planning in Average-Reward Markov Decision Processes](https://mlsanity.com/paper/2006.16318/) (2020) - [Q-learning with Nearest Neighbors](https://mlsanity.com/paper/1802.03900/) (2018) - [On Almost Sure Convergence Rates of Stochastic Gradient Methods](https://mlsanity.com/paper/2202.04295/) (2022) - [The ODE Method for Asymptotic Statistics in Stochastic Approximation and Reinforcement Learning](https://mlsanity.com/paper/2110.14427/) (2021) - [Average-Reward Off-Policy Policy Evaluation with Function Approximation](https://mlsanity.com/paper/2101.02808/) (2021) - [Concentration of Contractive Stochastic Approximation: Additive and Multiplicative Noise](https://mlsanity.com/paper/2303.15740/) (2023) - [The ODE Method for Stochastic Approximation and Reinforcement Learning with Markovian Noise](https://mlsanity.com/paper/2401.07844/) (2024) - [On Convergence of Emphatic Temporal-Difference Learning](https://mlsanity.com/paper/1506.02582/) (2015) - [Global Optimality and Finite Sample Analysis of Softmax Off-Policy Actor Critic under State Distribution Mismatch](https://mlsanity.com/paper/2111.02997/) (2021) - [Convergence Rates for Stochastic Approximation: Biased Noise with Unbounded Variance, and Applications](https://mlsanity.com/paper/2312.02828/) (2023) - [Almost Sure Convergence Rates and Concentration of Stochastic Approximation and Reinforcement Learning with Markovian Noise](https://mlsanity.com/paper/2411.13711/) (2024) - [Linear Q-Learning Does Not Diverge in L2: Convergence Rates to a Bounded Set](https://mlsanity.com/paper/2501.19254/) (2025) - [On Convergence of some Gradient-based Temporal-Differences Algorithms for Off-Policy Learning](https://mlsanity.com/paper/1712.09652/) (2017) - [Truncated Emphatic Temporal Difference Methods for Prediction and Control](https://mlsanity.com/paper/2108.05338/) (2021) - [Revisiting Step-Size Assumptions in Stochastic Approximation](https://mlsanity.com/paper/2405.17834/) (2024) - [Asymptotic and Finite Sample Analysis of Nonexpansive Stochastic Approximations with Markovian Noise](https://mlsanity.com/paper/2409.19546/) (2024) - [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020) - [Revisiting a Design Choice in Gradient Temporal Difference Learning](https://mlsanity.com/paper/2308.01170/) (2023) - [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022) - [Almost Sure Convergence of Linear Temporal Difference Learning with Arbitrary Features](https://mlsanity.com/paper/2409.12135/) (2024) ## Built on by (most cited first, 7 of 7) - [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026) - [AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theory](https://mlsanity.com/paper/2602.02285/) (2026) - [Almost Sure Convergence of Differential Temporal Difference Learning for Average Reward Markov Decision Processes](https://mlsanity.com/paper/2602.16629/) (2026) - [Almost Sure Convergence Rates of Stochastic Approximation and Reinforcement Learning via a Poisson-Moreau Drift](https://mlsanity.com/paper/2605.07104/) (2026) - [MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries](https://mlsanity.com/paper/2605.07147/) (2026) - [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026) - [ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization](https://mlsanity.com/paper/2609.34960/) (2026) ## Abstract (arXiv) 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.