# Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 33 references that are in the map.
- First posted on arXiv 11 Dec 2021.

## Builds on (most cited first, 2 of 2)

- [CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq](https://mlsanity.com/paper/2009.11403/) (2020)
- [An Evaluation of the Archive of Formal Proofs](https://mlsanity.com/paper/2104.01052/) (2021)

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

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes](https://mlsanity.com/paper/2206.02169/) (2022)

## Abstract (arXiv)

We present a formalisation of finite Markov decision processes with rewards in the Isabelle theorem prover. We focus on the foundations required for dynamic programming and the use of reinforcement learning agents over such processes. In particular, we derive the Bellman equation from first principles (in both scalar and vector form), derive a vector calculation that produces the expected value of any policy p, and go on to prove the existence of a universally optimal policy where there is a discounting factor less than one. Lastly, we prove that the value iteration and the policy iteration algorithms work in finite time, producing an epsilon-optimal and a fully optimal policy respectively.