Finite-horizon games

LeanMFG.Computational provides finite-horizon environments, policies, population evolution, Bellman recursion, numerical solvers, and tuning. These modules execute natively in Lean. The current environments and solvers draw on MFGLib 0.3.0, with numerical comparisons pinned to commit d4adccf134e88ad47e0a517af5175edaec15a30f. The solver reference checks are numerical tests. The shared sum and dot-product primitives have formal rounding-error bounds; correctness and convergence of whole solvers remain open.

General model

An Environment contains a horizon $T$, arbitrary finite state and action shapes $S$ and $A$, an initial distribution $\mu_0$, a reward scale rMax, and two callbacks:

Both callbacks can depend on time and the full joint state–action population $L_t$. A policy $\pi_t(a\mid s)$ induces the forward evolution

Rewards are collected at times $0,\ldots,T$, including the terminal time. Transitions run at $0,\ldots,T-1$. The Bellman recursion is undiscounted, matching the pinned implementation. When computing a best response or evaluating a deviating policy, the population sequence $L$ stays fixed.

The representation uses CPU Float (binary64) arrays in row-major order. The shared sum and dot functions use FloatLib's explicit nearest-even binary64 operations, converting at the array boundary. The forward state-population step calls the checked population kernel, with proved coordinate, L1, and mass-drift bounds. Other arithmetic, including Dual operations, transcendental functions, and handwritten accumulation loops, still uses native Float and is outside those primitive error theorems. Policy and mean-field shapes are (T+1, *S, *A); a reward slice has shape (*S, *A) and a transition slice has shape (*S_destination, *S_source, *A). S and A retain their multidimensional shapes; numerical loops use their products. Public policy constructors and solvers validate dimensions, finiteness, nonnegativity, and probability sums. This runtime validation is separate from the proof-carrying rational distributions used by earlier cases.

Environment callbacks operate on Dual values, which carry a value and one directional derivative. Ordinary forward evaluation uses zero derivative seeds. MFOMO seeds each variable in turn, so derivatives include the dependence of rewards and transitions on $L$. Custom callbacks should use Dual arithmetic for differentiable operations. The rounded transitions in Linear Quadratic have zero derivative through the rounding decision, following the upstream implementation.

Capability map

The solver implementations are in Iterative, MFOMO, and OccupationMeasure. The tuning interface accepts multiple environments and initial policies, records failed trials, and returns the best successful configuration. Random search uses the upstream parameter ranges and supports frozen fields.

Built-in environments

All definitions and parameter defaults are in Environments.lean.

The upstream rock–paper–scissors rewards are weighted. They are distinct from the everyday static game already proved in this repository. Beach Bar and Crowd Motion use clamped boundary movement, as the source code does, despite upstream descriptions referring to a torus.

Run

From the repository root:

lake build
lake exe mfglib_check
lake exe mfglib left_right omd 20
lake exe mfglib susceptible_infected fp 10
lake exe mfglib left_right mfomo 10
lake exe mfglib left_right omi 10

The solver command emits JSON containing the policy shape, full iteration history, and best index. Algorithms are fp, omd, pd, mfomo, and omi. lake exe mfglib --list lists all environments.

For full configuration, generate a JSON example, edit it, and run it:

lake exe mfglib --write-config /tmp/leanmfg-run.json
lake exe mfglib --config /tmp/leanmfg-run.json

The schema is RunConfig. It includes the environment's constructor arguments, algorithm parameters, optional initial policy, and stopping options. --tune FILE accepts a TuneConfig with environments, algorithm candidates, a metric, and solve options. Finite numerical values are written as exact decimal JSON numbers, preserving small tolerances and saved policy probabilities through parsing. Diagnostic terminal messages still use Lean's ordinary short Float display.

In Lean, import LeanMFG.Computational and call a solver directly:

open LeanMFG.Computational

def demo : IO Unit := do
  let result ← (OnlineMirrorDescent.solve { alpha := 0.2 }
    Environments.leftRight none { maxIter := 20 }).run
  match result with
  | .ok trace => IO.println trace.exploitabilities
  | .error message => IO.eprintln message

What the checks establish

The native check suite compares committed reference arrays generated by the pinned, unmodified Python source. It covers every environment, forward evolution, rewards, transitions, both Q recursions, greedy policies, exploitability, solver traces, occupation matrices, simplex/occupation projections, and MFOMO objectives and automatic derivatives for all three losses and both parameterizations. It also exercises invalid inputs, tied actions, zero-mass states, early stopping, tuning, and JSON serialization. Reference agreement uses explicit absolute and relative tolerances; it does not assert bitwise equality or correctness for every input.

Normal builds and checks need no Python. To regenerate the reference file, use Python 3.12, install tests/mfglib/requirements-oracle.txt, check out the pinned upstream commit in a separate directory, and run:

python scripts/mfglib_reference.py --upstream /path/to/MFGLib
lake exe mfglib_check

The generator rejects a different commit or a modified checkout and records the PyTorch version. Arithmetic tests use float64, except upstream OMI traces: its OSQP wrapper forces float32, so those runs use float32 throughout. Random coefficients and RNG fixtures use PyTorch's scalar CPU float32 sampling convention, reproduced by MT19937.

Differences and remaining work

• Numerical backend: arrays and loops run on the CPU with binary64 values. PyTorch tensor APIs, GPU execution, and bitwise equality to float32 runs are not provided. Dense matrices and forward automatic differentiation prioritize a direct executable implementation; large instances need performance work.
• OMI projection: native Dykstra iteration solves the same constrained Euclidean projection as the upstream OSQP call. It reports failure if its feasibility and complementarity tolerances are not reached. Warm starts and iteration counts differ from OSQP. Projection tolerances are explicit in the Lean configuration rather than inherited from outer stopping tolerances.
• Optimization and tuning: Adam and SGD are implemented, including SGD momentum. Arbitrary PyTorch optimizers and Optuna's TPE sampler, study database, pruning, and Python serialization formats remain outside this implementation. Native candidate search, seeded random search, frozen parameters, metrics, and JSON provide the corresponding basic workflow.
• Stable arithmetic: softmax and prior updates subtract a maximum before exponentiation; geometric means use logarithms. Parameterized hat initialization is compared through the probabilities it represents because logarithms amplify reduction roundoff near zero. The pinned upstream's augmented slack convention is retained.
• Explicit fixes: upstream Fictitious Play raises a shape error on multidimensional actions. The Lean implementation handles flattened action rows, and tests that case separately. For a custom MFOMO u, hat initialization uses the population represented by softmax(u); upstream instead passes raw u into its probability check. Inputs containing NaN or infinity are rejected.
• Proof scope: the shared sum and dot product have formal local and cumulative error bounds, conditional on finite inputs and intermediates. The one-step population update composes them into forward-error and mass-drift bounds, including explicit input perturbations. The numerical implementation has no whole-solver correctness, convergence, equilibrium-existence, or discretization-error theorems. rMax follows the upstream numerical scale and is not a certified bound. Existing rational and continuous proofs remain available in their original modules. A formal bridge to these numerical implementations is separate work.

Upstream attribution and license texts are preserved in the repository's third-party notices.