A lean proof that stationary policies can be optimal and can be computed using dynamic programming
See https://formalproofs.github.io/Probability
- 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/
- 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