Module organization
LeanMFG separates mathematical definitions, executable operations, and proofs about those operations. The following directories are relative to LeanMFG/.
| Directory | Contents |
|---|---|
Model/ | Rational static and one-step games; deterministic continuous control |
Theory/ | Equilibrium properties and classical HJB results |
Algorithm/ | Exact rational best responses and equilibrium checkers |
Computational/ | Finite-horizon environments, policies, Bellman recursion, numerical solvers, tuning, and CLI |
Numerical/ | Binary64 reductions and the checked forward population kernel |
Verification/ | Correctness and error theorems connected to the executable definitions |
Examples/ | Concrete games, control problems, and executable guards |
The mathematical directories use Static/, FiniteState/, and Continuous/ subdirectories. Numerical proofs live in Verification/Numerical/.
Library entry points
import LeanMFG imports the complete library and its proved examples. import LeanMFG.Computational imports the numerical interface. Individual files can be imported directly when a client needs a smaller part of the library.
The Lake targets are LeanMFG, mfglib, and mfglib_check. The first builds the library; the other two provide the numerical command and reference-test executable.
Mathematical and numerical representations
The rational models carry nonnegativity and normalization proofs in their distribution types. Continuous-control models use real-valued functions and explicit smoothness and integrability hypotheses.
The computational model uses flat binary64 arrays and runtime validation. Its policies and joint populations both have shape (T + 1, *S, *A), with different meanings. Reward and policy indices include the terminal time; transitions use times 0 through T - 1. See the finite-horizon guide for the array convention.
These representations have separate interfaces. The RPS adapter relates the original three-action game to the generic finite static model. The numerical verification modules relate selected FloatLib operations to exact real-valued expressions. The verification table records the scope of each connection.
Dependencies
The repository pins Lean in lean-toolchain, direct dependencies in lakefile.toml, and the resolved dependency graph in lake-manifest.json.
- mathlib supplies finite sums, ordered algebra, real analysis, integration, and proof tactics.
- FloatLib supplies the binary64 operations and arithmetic semantics used by the numerical kernels.
MFGLib is a reference for the current numerical environments and algorithms. Its Python packages are needed only to regenerate comparison fixtures. Normal Lean builds and numerical checks use the committed fixtures.
Adding a module
Place definitions according to their role above, import them from the appropriate library entry point, and add an example that exercises the public interface. Update the verification scope if the change adds or changes a guarantee. The contribution guide lists the checks to run.