Formalise the policy gradient theorem for finite discounted MDPs in Lean 4
Difficulty 18: textbook mathematics; the work is building finite-MDP infrastructure (occupancy measures, softmax derivatives) in Mathlib, more than PutnamBench reproduction (8) but far below a kernel-conformance proof (52). Application value 6. Leverage 15: a base for later formal RL theory.
The problem
Have a computer proof checker verify the basic formula behind policy-gradient learning.
- 1Define a small decision world
- 2Show rule value is well defined
- 3Compare two rules exactly
- 4Prove the gradient formula
- 5Machine checks every step
Why it matters. RL theory papers contain long calculations, and errors in published proofs do occur. A proof assistant such as Lean checks every step of a proof mechanically, and Mathlib is its large shared library of formalised mathematics. Formalising the basic theorems of RL would give a checked foundation on which later results, such as convergence of PPO-style methods, can be built and machine-verified, and a test set for AI theorem provers.
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Policy gradient methods and PPOAlgorithm · host
- Then
- Formalise the policy gradient theorem for finite discounted MDPs in Lean 4The problem
State of the art
Mathlib has the Banach fixed-point theorem for contracting maps (Mathlib/Topology/MetricSpace/Contracting.lean, ContractingWith.fixedPoint), so step (1) reduces to showing the Bellman operator contracts. Zhang's rl-theory-in-lean project (arXiv 2511.03618, RL Journal 2026) formalises almost-sure convergence of Q-learning and linear TD with the Robbins-Siegmund theorem in Lean 4 on Mathlib. Bellman optimality for finite MDPs has been formalised in other provers (Isabelle/AFP, Coq), and Zhang's paper describes earlier Lean work as dynamic programming rather than RL. No public Lean 4 formalisation of the performance difference lemma or of the policy gradient theorem was found in Mathlib, in rl-theory-in-lean or by a search on 2026-10-17; anyone starting should check the Lean Zulip first.
Realistic applications
A verified base for later formal proofs of convergence of policy optimisation (natural policy gradient, PPO-style updates), and a test bed for AI theorem provers on RL theory.
What counts as solved
A Lean 4 development, compiled against a stated Mathlib version with no sorry and no new axioms, proving all three statements, accepted into a public repository or Mathlib-style library.
How it gets verified
Lean proofA formal proof checked by Lean 4 / Mathlib.
Route: Lean 4 + Mathlib, checked by lake build against a stated Mathlib commit with zero sorry and #print axioms showing only propext, Classical.choice and Quot.sound. Mathlib has the fixed-point theorem (ContractingWith.fixedPoint in Mathlib/Topology/MetricSpace/Contracting.lean) but no MDP, policy-value or occupancy-measure library; rl-theory-in-lean provides stochastic-approximation tools but not this theorem. Sketch only, not type-checked (the formaliser fixes the final form):
structure FiniteMDP (S A : Type) [Fintype S] [Fintype A] where
P : S → A → S → ℝ -- transition probabilities, nonneg, rows sum to 1
r : S → A → ℝ
γ : ℝ
hγ : 0 ≤ γ ∧ γ < 1
-- softmax policy, value V^π as the fixed point of the Bellman operator, J θ = Σ_s μ s * V^{π_θ} s
theorem policy_gradient (M : FiniteMDP S A) (μ : S → ℝ) (θ : S → A → ℝ) :
HasFDerivAt (fun θ => J M μ θ) (pgGradient M μ θ) θ := by
sorry
where pgGradient is the occupancy-weighted sum , and the contraction and performance-difference lemmas are proved as separate theorems.
Claims under verification
+ add a claimNo claimed results on the Verification board for this problem yet.
Where the work is
Formalisation effort; the mathematics is classical.
Bottlenecks
ranked by votes- #1EngineeringMissing MDP infrastructure in Mathlib
Discounted occupancy measures, policy values and differentiation of finite sums of softmax terms must be built, and design choices affect later reuse.
Community grades
Sign in to add your own grade.
Connected problems
No connections yet.
Progress
- Nov 5, 2025Q-learning and TD convergence in Leansource
Zhang formalises almost-sure convergence of Q-learning and linear TD (preprint).