Formalizing Markov Decision Processes in Lean

Verified Lean algorithms for tabular MDPs, with two goals:

1. Algorithms that solve robust and risk-averse MDPs of moderate size.
2. Proofs of correctness and of fundamental MDP properties, usable on their own for structural results such as the optimality of a policy class.

The API documentation and the companion paper are published by CI on every push to main.

Library Contents

Sample spaces are finite ([FinEnum Ω]), so there are no measurability side conditions. Two types appear:

• W: probabilities, and values that are averaged with them (expectation, CVaR). Any linear ordered field — ℚ makes every definition computable (see MDPLibTest.lean), ℝ gives the standard theory.
• V: values that are only compared (events, ℙ, CDF, quantiles, VaR). Any linear order, e.g. W, ℕ, ℤ.

They are separate so that order-only results apply to any ordered values, and so that @[to_dual (dont_translate := W)] can derive mirror-image results by reversing the order on values without reversing it on probabilities.

Mathlib's measure-theoretic probability is not used: it is noncomputable, fixed to ℝ/ℝ≥0∞, and has no quantiles or VaR. Its scalar-generic convexity API (Finset.centerMass, StdSimplex) is reused instead.

Probability foundations

MDPLib/Probability/Defs.lean, MDPLib/Probability/Prelude.lean

Result	Lean name
Finite distribution on Ω (nonneg weights summing to one), Dirac distribution	Findist, Findist.Δ, Findist.dirac
A distribution forces its sample space to be nonempty	Findist.nonempty
Random variables as bare functions Ω → V; events as Ω → Bool with Mathlib's Boolean algebra (⊔, ⊓)	FinRV, FinRV.sup_eq_or, FinRV.inf_eq_and
Comparison events X ≤ᵣ t, X <ᵣ t, X ≥ᵣ t, X >ᵣ t, X =ᵣ y and the indicator 𝕀	FinRV.leq, FinRV.lt, FinRV.geq, FinRV.gt, FinRV.eq, FinRV.indicator
Probability ℙ[B // P], conditional probability ℙ[B | C // P]	Findist.probability, Findist.probabilityCond
Expectation 𝔼[X // P], conditional expectation 𝔼[X | B // P] and the conditional-expectation random variable 𝔼[X |ᵣ L // P]	Findist.expect, Findist.expectCond, Findist.expectCondRV
Probability as the expectation of an indicator	Findist.probability_eq_expect_indicator
Decomposition of a random variable along a discrete label X = ∑ᵢ X · 𝕀[L = i]	FinRV.eq_sum_mul_indicatorEq, Findist.expect_eq_sum_mul_indicatorEq
Convexity bounds for two-point mixtures; Jensen's inequality for |·| on the uniform distribution	IsProb.self_le_combo_of_le, IsProb.combo_le_self_of_ge, Matrix.abs_dotProduct_le_dotProduct_abs_uniform

Expectation as a convex combination

MDPLib/Probability/Convexity.lean

Result	Lean name
𝔼[X // P] is Mathlib's Finset.centerMass at weights summing to one	Findist.expect_eq_centerMass
minQuark X ≤ 𝔼[X] ≤ maxQuark X	Findist.expect_ge_minQuark, Findist.expect_le_maxQuark
Jensen's inequality for an arbitrary convex / concave function	Findist.expect_convexOn_le, Findist.expect_concaveOn_ge

Bridge to Mathlib's standard simplex

MDPLib/Probability/StdSimplex.lean

Result	Lean name
A Findist as a point of Convexity.StdSimplex (noncomputable; proof-layer only)	Findist.toStdSimplex
Mathlib's indexed convex combination is this library's expectation	Findist.toStdSimplex_iConvexComb
Findist.dirac is StdSimplex.single; the bridge is injective	Findist.toStdSimplex_dirac, Findist.toStdSimplex_injective

Probability: basic properties

MDPLib/Probability/Basic.lean

Result	Lean name
ℙ takes values in [0,1]	Findist.probability_nonneg, Findist.probability_le_one, Findist.isProb_probability
Linearity, homogeneity and monotonicity of expectation	Findist.expect_sum, Findist.expect_smul, Findist.expect_mono
Complement rules ℙ[B] + ℙ[¬B] = 1, and the ≤/> and </≥ pairs	Findist.probability_add_probability_not, Findist.probability_le_gt_one, Findist.probability_lt_ge_one
Monotonicity of ℙ[X ≤ t] in both X and t (and the antitone versions)	Findist.probability_le_mono, Findist.probability_lt_mono, Findist.probability_ge_anti, Findist.probability_gt_anti
Behaviour of events and probabilities under monotone / strictly monotone / antitone transformations of X	FinRV.leq_eq_comp_leq_of_strictMono, StrictMono.probability_le, StrictMono.probability_ge, …
Cash (translation) invariance and negation duality of the comparison events	Findist.probability_leq_add_const, Findist.probability_leq_eq_neg_geq_neg
CDF cdf P X t = ℙ[X ≤ t]; it is nondecreasing in t and antitone in X	Findist.cdf, Findist.cdf_mono, Findist.cdf_anti_of_le
Law of the unconscious statistician	Findist.expect_comp_eq_sum
Tower property (law of total expectation)	Findist.expect_expectCondRV
Law of total probability	Findist.probability_eq_sum
Expectation equals the sum over the (finite) image of X	Findist.expect_eq_sum_probability_mul, FinRV.sum_image_univ_eq_sum_fin
Duplicate-free list of the values of a random variable, with index/value inverses	FinRV.imageList, FinRV.imageIdxOf, FinRV.getElem_imageIdxOf, FinRV.imageList_nodup
Invariance of probability and expectation under a permutation of the sample space	Findist.comp, Findist.probability_comp_perm, Findist.expect_comp_perm
A ≤ event can be replaced by a strict < event at a larger threshold	Findist.exists_probability_leq_eq_probability_lt, Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark

Quantiles

MDPLib/Probability/Quantile.lean

Result	Lean name
Quantile set {q | ℙ[X ≤ q] ≥ α ∧ ℙ[X ≥ q] ≥ 1-α} and its one-sided (lower) relaxation	Statistic.quantile, Statistic.quantileLower, Statistic.IsQuantile, Statistic.IsQuantileLower
Equivalent characterizations of membership, including the strict form ℙ[X < q] ≤ α	Statistic.mem_quantile_iff, Statistic.mem_quantileLower_iff_probability_lt, Statistic.mem_quantile_of_probability_lt
Every quantile is a lower quantile	Statistic.quantile_subset_quantileLower
Reflection: q is an α-quantile of X iff -q is a (1-α)-quantile of -X	Statistic.mem_quantile_neg_iff
Quantiles under monotone maps; equivalence for strictly monotone maps	Statistic.mem_quantile_comp_of_monotone, Statistic.mem_quantile_comp_iff_of_strictMono, Statistic.mem_quantileLower_comp_iff_of_strictMono
Lower quantiles of X ≤ Y are cofinal — the basis for monotonicity of VaR	Statistic.isCofinalFor_quantileLower_of_le
Cash invariance of the lower-quantile set: QuantileLower(X + c) = QuantileLower(X) + c	Statistic.quantileLower_add_const_eq_image
The image f '' quantile(X) is cofinal/coinitial in quantile(f∘X) for monotone f (proof incomplete)	Statistic.isCofinalFor_quantile_comp_image_of_monotone, Statistic.isCoinitialFor_quantile_comp_image_of_monotone

Value at Risk

MDPLib/Risk/VaR.lean

Result	Lean name
Risk level 0 ≤ α < 1	Risk.IsRiskLevel, Risk.RiskLevel
Non-constructive VaR: the greatest lower quantile (equivalently, the greatest quantile)	Risk.IsVaR, Risk.IsVaRQuantile
Characterization IsVaR v ↔ ℙ[X < v] ≤ α < ℙ[X ≤ v]	Risk.isVaR_iff
Computable VaR VaR[X // P, α] as a max over the finite candidate set, which is nonempty	Risk.finVaR, Risk.finVaRSet, Risk.finVaRSet_nonempty
VaR is monotone: X ≤ Y implies VaR[X] ≤ VaR[Y]	Risk.IsVaR.le_of_le
Correctness of the computable VaR: IsVaR P X α (VaR[X // P, α])	Risk.isVaR_finVaR
The two definitions (greatest quantile / greatest lower quantile) agree	Risk.isVaRQuantile_iff_isVaR
The quantile set is nonempty	Risk.quantile_nonempty
Translation (cash) invariance for the Risk.IsVaR predicate	Risk.IsVaR.add_const
… and for the computable VaR: VaR[X + c] = VaR[X] + c	Risk.finVaR_add_const
Strictly monotone transformations for the Risk.IsVaR predicate	Risk.IsVaR.comp_of_strictMono
… and for the computable VaR: VaR[f∘X] = f(VaR[X])	Risk.finVaR_comp_of_strictMono
Positive homogeneity: VaR[c·X] = c·VaR[X] for c > 0	Risk.finVaR_const_mul

Main.lean checks VaR on the distributions in test_var.json using standalone code (computeVaR), not the verified Risk.finVaR.

MDPs and histories

MDPLib/MDP/Histories.lean

Result	Lean name
Tabular MDP with finite states, actions, transitions and rewards	MDP
Histories s₀ a₀ s₁ …, their length, last state, prefixes, and the length-indexed subtype	Hist, Hist.length, Hist.last, Hist.prefix, MDP.HistOfLength
The count S · (S·A)^t and the explicit index maps Fin (numHist t) ↔ HistOfLength t	MDP.numHist, MDP.idxToHist, MDP.histToIdx
… that those maps are mutually inverse, i.e. that the count is the cardinality (proof incomplete)	leftInverse_idxToHist_histToIdx, rightInverse_idxToHist_histToIdx, exists_init_of_length_eq_zero, exists_foll_of_length_eq_succ
Embeddings Hist × A × S ↪ Hist and S ↪ Hist	tupleToHistEmbedding, stateToHistEmbedding
The horizon-t history sets are exactly the histories of length t; Fintype (M.HistOfLength t)	mem_historiesHorizon, length_eq_of_mem_historiesHorizon, MDP.historiesHorizonT

The ℋ h t family is defined; its length lemma length_of_mem_histories is still unproven. MDPLib/Risk/CVaR.lean is a stub with notes for CVaR.

Building and testing

lake build MDPLib            # the library
lake -R build MDPLib:docs    # the API documentation
lake build mdplib            # the binary file
lake build MDPLibTest        # computability tests
./test.sh                    # computability + regression tests, interpreted and compiled (Linux)

CI runs the library build, test.sh, the docs and the paper on every pull request.

Lean Resources

Most useful

• Overview of tactics: https://github.com/madvorak/lean4-tactics
• Comprehensive list of tactics: https://seasawher.github.io/mathlib4-help/tactics/
• Loogle: https://loogle.lean-lang.org/
• Moogle: https://www.moogle.ai/

Others

• Blueprint: https://github.com/PatrickMassot/leanblueprint
• Lean packages and extensions: https://reservoir.lean-lang.org/
• Notations: https://github.com/leanprover-community/lean4-mode/blob/master/data/abbreviations.json
• Resource for Probability: https://korivernon.com/documents/MathematicalStatisticsandDataAnalysis3ed.pdf