Installation

LeanMFG requires Lean 4.34.0. Install elan, which selects the toolchain recorded by a Lean project. The numerical library runs on the CPU and does not require Python.

Install the library

Use a repository checkout to run the command-line solver and examples. These commands select the source commit used for this documentation:

git clone https://github.com/Varifold-Lab/LeanMFG.git
cd LeanMFG
git checkout 682517952b8fb92d488543baec7fb6dbbd6e0598
lake exe cache get
lake build LeanMFG mfglib mfglib_check

The cache command downloads compiled mathlib artifacts. The first build also compiles the required FloatLib modules.

Use the matching lean-toolchain in your project:

text

leanprover/lean4:v4.34.0

Add LeanMFG to your lakefile.toml:

toml

[[require]]
name = "leanmfg"
git = "https://github.com/Varifold-Lab/LeanMFG.git"
rev = "682517952b8fb92d488543baec7fb6dbbd6e0598"

Resolve and build the dependencies:

lake update
lake exe cache get
lake build

Commit the generated lake-manifest.json. Use the selected LeanMFG commit's mathlib and FloatLib versions together.

Check an import

This example uses a proved equilibrium statement:

lean

import LeanMFG

example : LeanMFG.RPS.IsEquilibrium LeanMFG.RPS.uniform :=
  LeanMFG.RPS.uniform_equilibrium

For numerical code, use import LeanMFG.Computational. The downstream client exercises both interfaces in a fresh Lake project during CI.

Run a solver

From a repository checkout:

lake exe mfglib left_right omd 20

Continue with Run a first solver to read the output and call the solver from Lean.

Dependency changes

The package's Lean toolchain and dependency commits form a tested combination. When upgrading LeanMFG, update the toolchain and resolve the dependency manifest together. The release guide describes compatibility changes between versions.

Instructions for editing this website are in Contributing.