mlsanityData to 14 Oct 2026

Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach

arXiv 2511.03618 ↗First posted 5 Nov 2025cs.LG stat.MLcited by 7

On the map: Deep reinforcement learning methods → RL theory and sample complexity

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.

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.

Builds on

37 of 82 references.

Closest ancestors · 6

Same direction, newest first

  1. 2025Extensions of Robbins-Siegmund Theorem with Applications in Reinforcement Learning30 Sep
  2. 2025Finite Sample Analysis of Linear Temporal Difference Learning with Arbitrary Features27 May
  3. 2025Linear Q-Learning Does Not Diverge in L2: Convergence Rates to a Bounded Set31 Jan
  4. 2024Almost Sure Convergence Rates and Concentration of Stochastic Approximation and Reinforcement Learning with Markovian Noise20 Nov
  5. 2024Almost Sure Convergence of Linear Temporal Difference Learning with Arbitrary Features18 Sep
  6. 2024The ODE Method for Stochastic Approximation and Reinforcement Learning with Markovian Noise15 Jan

Other references · 31

  1. 2020On the Global Convergence Rates of Softmax Policy Gradient Methodscited by 264
  2. 2018A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximationcited by 229
  3. 2019On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shiftcited by 177
  4. 2019Finite-Time Error Bounds For Linear Stochastic Approximation and TD Learningcited by 166
  5. 2019The Lean mathematical librarycited by 134
  6. 2015An Emphatic Approach to the Problem of Off-policy Temporal-Difference Learningcited by 103
  7. 2020Finite-Time Analysis of Asynchronous Stochastic Approximation and Q-Learningcited by 96
  8. 2020Sample Complexity of Asynchronous Q-Learning: Sharper Analysis and Variance Reductioncited by 95
  9. 2021Is Q-Learning Minimax Optimal? A Tight Sample Complexity Analysiscited by 92
  10. 2019Finite-Sample Analysis for SARSA with Linear Function Approximationcited by 85
  11. 2020Learning and Planning in Average-Reward Markov Decision Processescited by 54
  12. 2018Q-learning with Nearest Neighborscited by 37
19 more
  1. 2022On Almost Sure Convergence Rates of Stochastic Gradient Methodscited by 35
  2. 2021The ODE Method for Asymptotic Statistics in Stochastic Approximation and Reinforcement Learningcited by 32
  3. 2021Average-Reward Off-Policy Policy Evaluation with Function Approximationcited by 31
  4. 2023Concentration of Contractive Stochastic Approximation: Additive and Multiplicative Noisecited by 26
  5. 2015On Convergence of Emphatic Temporal-Difference Learningcited by 21
  6. 2021Global Optimality and Finite Sample Analysis of Softmax Off-Policy Actor Critic under State Distribution Mismatchcited by 17
  7. 2023Convergence Rates for Stochastic Approximation: Biased Noise with Unbounded Variance, and Applicationscited by 15
  8. 2017On Convergence of some Gradient-based Temporal-Differences Algorithms for Off-Policy Learningcited by 11
  9. 2021Truncated Emphatic Temporal Difference Methods for Prediction and Controlcited by 10
  10. 2024Revisiting Step-Size Assumptions in Stochastic Approximationcited by 10
  11. 2024Asymptotic and Finite Sample Analysis of Nonexpansive Stochastic Approximations with Markovian Noisecited by 10
  12. 2020CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coqcited by 9
  13. 2023Revisiting a Design Choice in Gradient Temporal Difference Learningcited by 7
  14. 2022Formalization of a Stochastic Approximation Theoremcited by 5
  15. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  16. 2021Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOLcited by 3
  17. 2024Formalization of Complexity Analysis of the First-order Algorithms for Convex Optimizationcited by 2
  18. 2025A Formalization of the Ionescu-Tulcea Theorem in Mathlibcited by 2
  19. 2024Formally Verified Approximate Policy Iterationcited by 1

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 7.

7 papers.

  1. 2026LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalizationcited by 12
  2. 2026AI4SLT: Empirical Processes in Lean 4 for Formal Statistical Learning Theorycited by 5
  3. 2026Almost Sure Convergence of Differential Temporal Difference Learning for Average Reward Markov Decision Processescited by 2
  4. 2026Almost Sure Convergence Rates of Stochastic Approximation and Reinforcement Learning via a Poisson-Moreau Driftcited by 1
  5. 2026MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Librariescited by 1
  6. 2026Lean Pool: An AI-Maintained Archive of Formalized Mathematicscited by 1
  7. 2026ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimizationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Convergence and stability of Q-learning in Hierarchical Reinforcement Learning
  2. 2026Mathematical methods of reinforcement learning
  3. 2026Commit to the Bit: Reactive Reinforcement Learning Done Right
  4. 2024Theoretical Analysis of Meta Reinforcement Learning: Generalization Bounds and Convergence Guarantees
  5. 2024PID Accelerated Temporal Difference Algorithms
  6. 2019On Value Functions and the Agent-Environment Boundary
  7. 2023Understanding Reinforcement Learning Algorithms: The Progress from Basic Q-learning to Proximal Policy Optimization
  8. 2025Rethinking the Foundations for Continual Reinforcement Learning