formalproofsmdplib0.1.0

Formalization of MDP Theory

Formalizing Markov Decision Processes in Lean

CI Documentation

Documentation: the API documentation and the companion paper are built by CI and published to GitHub Pages on every push to main.

Verified Lean algorithms for solving tabular MDPs and proving their properties. The focus of this project is on two main goals:

  1. Basic algorithms that can solve robust and risk-averse MDPs of moderate size.

  2. Proofs of correctness of algorithms and fundamental MDP properties which can be used independently to prove structural results, such as the optimality of certain policy class.

Library Contents

The main results formalized so far. Everything is developed for finite sample spaces ([FinEnum Ω]) over an arbitrary linear ordered field R ([Field R] [LinearOrder R] [IsStrictOrderedRing R] [CharZero R] [Archimedean R]), so the statements are free of measurability side conditions. Instantiate at ℚ — as MDPLibTest.lean does — and every definition is computable and executable; instantiate at ℝ for the standard theory, where the definitions remain well-formed but noncomputable (Real.instField and the classical DecidableLE ℝ are noncomputable, so VaR[X // P, α] cannot be #eval'd over ℝ).

Relationship to Mathlib's measure theory-based probability

Mathlib's measure-theoretic probability (Measure, PMF, ∫, ∫⁻) is not used, and cannot be: it is uniformly noncomputable and valued in ℝ≥0∞ or an ℝ-normed space, so it neither evaluates at ℚ nor says anything about a general scalar R. Mathlib also has no quantiles, VaR or CVaR at all. What is reused is the scalar-generic algebraic API — Finset.centerMass, which is weighted expectation over exactly this library's class stack, and the order/convexity results built on it. See the audit note at the top of MDPLib/Probability/Defs.lean for the details and citations.

Legend: ✅ proof complete  ·  🚧 statement final, proof still depends on a sorry (check with #print axioms).

Probability foundations

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

ResultLean name
✅Finite distribution on Ω (nonneg weights summing to one), Dirac distributionFindist, Findist.Δ, Findist.dirac
✅A distribution forces its sample space to be nonemptyFindist.nonempty
✅Random variables as bare functions Ω → ρ; events as Ω → Bool with a Boolean semiring structureFinRV, FinRV.instMulBool, FinRV.instAddBool
✅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 indicatorFindist.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 distributionIsProb.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

ResultLean name
✅𝔼[X // P] is Mathlib's Finset.centerMass at weights summing to oneFindist.expect_eq_centerMass
✅min X ≤ 𝔼[X] ≤ max XFindist.expect_ge_min, Findist.expect_le_max
✅Jensen's inequality for an arbitrary convex / concave functionFindist.expect_convexOn_le, Findist.expect_concaveOn_ge

Bridge to Mathlib's standard simplex

MDPLib/Probability/StdSimplex.lean

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

Probability: basic properties

MDPLib/Probability/Basic.lean

ResultLean name
✅ℙ takes values in [0,1]Findist.probability_nonneg, Findist.probability_le_one, Findist.isProb_probability
✅Linearity, homogeneity and monotonicity of expectationFindist.expect_sum, Findist.expect_smul, Findist.expect_mono
✅Complement rules ℙ[B] + ℙ[¬B] = 1, and the ≤/> and </≥ pairsFindist.probability_add_probability_not, Findist.probability_leq_add_probability_gt, Findist.probability_lt_add_probability_geq
✅Monotonicity of ℙ[X ≤ t] in both X and t (and the antitone versions)Findist.probability_leq_mono, Findist.probability_lt_mono, Findist.probability_geq_anti, Findist.probability_gt_anti
✅Behaviour of events and probabilities under monotone / strictly monotone / antitone transformations of XFinRV.leq_eq_comp_leq_of_strictMono, StrictMono.probability_leq_eq, StrictMono.probability_geq_eq, …
✅Cash (translation) invariance and negation duality of the comparison eventsFindist.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 XFindist.cdf, Findist.cdf_mono, Findist.cdf_anti_of_le
✅Law of the unconscious statisticianFindist.expect_comp_eq_sum
✅Tower property (law of total expectation)Findist.expect_expectCondRV
✅Law of total probabilityFindist.probability_eq_sum
✅Expectation equals the sum over the (finite) image of XFindist.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 inversesFinRV.imageList, FinRV.imageIdxOf, FinRV.getElem_imageIdxOf, FinRV.imageList_nodup
✅Invariance of probability and expectation under a permutation of the sample spaceFindist.comp, Findist.probability_comp_perm, Findist.expect_comp_perm
🚧A ≤ event can be replaced by a strict < event at a larger thresholdFindist.exists_probability_leq_eq_probability_lt_of_lt_max

Probability: matrices and Markov reward processes

MDPLib/Probability/Matrix.lean

ResultLean name
✅Row-stochastic transition matrixMatrix.ProbabilityMatrix
✅A distribution pushed through a transition matrix is again a distributionMatrix.nonneg_vecMul, Matrix.vecMul_dotProduct_one
✅Discounted Markov reward process and its Bellman backup 𝔹[v // Proc] = r + γ · P vMatrix.DiscountedMRP, Matrix.bellmanBackup

Quantiles

MDPLib/Probability/Quantile.lean

ResultLean name
✅Quantile set {q | ℙ[X ≤ q] ≥ α ∧ ℙ[X ≥ q] ≥ 1-α} and its one-sided (lower) relaxationStatistic.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 quantileStatistic.quantile_subset_quantileLower
✅Reflection: q is an α-quantile of X iff -q is a (1-α)-quantile of -XStatistic.mem_quantile_neg_iff
✅Quantiles under monotone maps; equivalence for strictly monotone mapsStatistic.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 VaRStatistic.isCofinalFor_quantileLower_of_le
✅Cash invariance of the lower-quantile set: QuantileLower(X + c) = QuantileLower(X) + cStatistic.quantileLower_add_const_eq_image
🚧The image f '' quantile(X) is cofinal/coinitial in quantile(f∘X) for monotone fStatistic.isCofinalFor_quantile_comp_image_of_monotone, Statistic.isCoinitialFor_quantile_comp_image_of_monotone

Value at Risk

MDPLib/Risk/VaR.lean

ResultLean name
✅Risk level 0 ≤ α < 1Risk.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 nonemptyRisk.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) agreeRisk.isVaRQuantile_iff_isVaR
🚧The quantile set is nonemptyRisk.quantile_nonempty
✅Translation (cash) invariance for the Risk.IsVaR predicateRisk.IsVaR.add_const
🚧… and for the computable VaR: VaR[X + c] = VaR[X] + cRisk.finVaR_add_const
✅Strictly monotone transformations for the Risk.IsVaR predicateRisk.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 > 0Risk.finVaR_const_mul

The 🚧 entries above are all complete modulo the single missing lemma Findist.exists_probability_leq_eq_probability_lt_of_lt_max.

Main.lean contains an executable that reads distributions from a JSON file, computes VaR with computeVaR, and checks it against reference values (see test_var.json). computeVaR is standalone IO glue over Array ℚ rather than the verified Risk.finVaR; it is MDPLibTest.lean that instantiates the library itself at ℚ.

MDPs and histories

MDPLib/MDP/Histories.lean

ResultLean name
✅Tabular MDP with finite states, actions, transitions and rewardsMDP
✅Histories s₀ a₀ s₁ …, their length, last state, prefixes, and the length-indexed subtypeHist, Hist.length, Hist.last, Hist.prefix, MDP.HistOfLength
✅The count S · (S·A)^t and the explicit index maps Fin (numHist t) ↔ HistOfLength tMDP.numHist, MDP.idxToHist, MDP.histToIdx
🚧… that those maps are mutually inverse, i.e. that the count is the cardinalityleftInverse_idxToHist_histToIdx, rightInverse_idxToHist_histToIdx, exists_init_of_length_eq_zero, exists_foll_of_length_eq_succ
✅Embeddings Hist × A × S ↪ Hist and S ↪ HisttupleToHistEmbedding, 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 (histories extending h by t steps) is defined but its length lemma length_of_mem_histories is still 🚧.

MDPLib/Risk/CVaR.lean is an empty stub; it carries notes on which Mathlib pieces are and are not available for Conditional Value at Risk.

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        # tests the elaborationa dn

On linux, you can use build and test the binary file as follows:

./test.sh                    # computability + regression tests, interpreted and compiled

CI (.github/workflows/ci.yml) runs the library build, that script, the docs and the paper on every pull request, and deploys to GitHub Pages on main.

Lean Resources

Most useful

Others