LeanMFG documentation
LeanMFG is a Lean 4 library for formal mean field games. It connects mathematical models, theory, executable algorithms, and formal verification. Current results include finite-game equilibria, classical HJB verification, and numerical error bounds, alongside finite-horizon solvers and examples.
Using the library
Install LeanMFG to run the numerical solvers or import its definitions into a Lean project. The first solver example solves a Left/Right game and explains how to inspect the policy and exploitability history.
lake exe mfglib left_right omd 20The API reference documents the solver interface, options, result types, and population update. The finite-horizon guide covers array layout, built-in environments, tuning, and numerical conventions.
Mathematical examples
| Example | Model | Results |
|---|---|---|
| Rock-paper-scissors | Rational mixed strategies | Best response, equilibrium checker, unique uniform equilibrium |
| Finite static games | Arbitrary finite nonempty action type | Pure-deviation characterization and an RPS adapter |
| Left/Right | Rational one-step dynamics | Population conservation and equilibrium verification |
| Deterministic HJB | One-dimensional continuous control | Classical verification and an optimal feedback path |
| Population update | Binary64 arrays | Coordinate error and mass-drift bounds |
Numerical solver output is a floating-point approximation. The verification guide lists the results covered by proofs and the checks applied to the numerical implementation.
Developing LeanMFG
Join the community discussion on Lean Zulip or WeChat to ask questions and suggest directions for the library.
See module organization for the source layout, contributing for local commands and documentation conventions, and releases for versioning and publication.