LeanMFGdocumentation

Try “exploitability”, “HJB”, or “SolveOptions”.

GitHub ↗

Static rock-paper-scissors

One population distribution, one representative player, and an executable certificate for the most that player can gain by changing strategy.

This example is inspired by §2.1, Example 2 of Learning in Mean Field Games: A Survey. It uses the everyday convention: a win earns +1, a loss earns −1, and a tie earns 0. The survey displays the opposite cyclic reward signs, so the formulas below are not transcribed from its payoff formulas.

Model

The action set is Rock, Paper, Scissors. A distribution stores rational probabilities, proof that each is nonnegative, and proof that their sum is one:

mR,mP,mS∈Q≥0,mR+mP+mS=1.m_R,m_P,m_S \in \mathbb{Q}_{\geq 0}, \qquad m_R+m_P+m_S=1.

The personal mix p and population mix m have the same type but different roles. A unilateral deviation changes p while m remains fixed. Pure-action rewards are

r(R,m)=mS−mP,r(P,m)=mR−mS,r(S,m)=mP−mR.\begin{aligned} r(R,m)&=m_S-m_P,\\ r(P,m)&=m_R-m_S,\\ r(S,m)&=m_P-m_R. \end{aligned}

The player's expected reward is

J(p;m)=∑a∈{R,P,S}par(a,m).J(p;m)=\sum_{a\in\{R,P,S\}}p_a r(a,m).

Equilibrium

At an exact equilibrium, no rational personal mix improves the reward against fixed m:

∀p,J(p;m)≤J(m;m).\forall p,\qquad J(p;m)\leq J(m;m).

An ε-equilibrium requires ε ≥ 0 and permits improvement of at most ε:

∀p,J(p;m)≤J(m;m)+ε.\forall p,\qquad J(p;m)\leq J(m;m)+\varepsilon.

Population consistency is exact: the representative strategy being certified is m itself. The first version quantifies over rational mixed strategies.

Executable certificate

bestResponse m compares the three pure rewards and returns a maximizer. Ties favor Rock, then Paper, then Scissors. Exploitability is

exploitability⁡(m)=r(bestResponse⁡(m),m)−J(m;m).\operatorname{exploitability}(m) =r(\operatorname{bestResponse}(m),m)-J(m;m).

The Boolean checkEpsilonEquilibrium m ε accepts exactly when ε ≥ 0 and exploitability is at most ε.

What Lean proves

The verification theorems show that the actual executable bestResponse returns a maximizing action; every rational mixed strategy scores no higher; exploitability is nonnegative; and the Boolean checker accepts if and only if the quantified ε-equilibrium definition holds.

The merged exploitability_eq_zero_iff theorem connects the numerical gain directly to exact equilibrium:

exploitability⁡(m)=0⟺m is an exact equilibrium.\operatorname{exploitability}(m)=0 \quad\Longleftrightarrow\quad m\text{ is an exact equilibrium}.

If gain is zero, the best-response bound rules out every mixed deviation. Conversely, an equilibrium rules out improvement by the pure best response, so exploitability is at most zero; nonnegativity gives equality. The population m remains fixed in both directions. Combined with uniqueness, this shows that zero exploitability forces the uniform distribution; the example module includes this proof.

The theory module shows self-play has reward zero. At equilibrium, each pure reward is at most zero; the three rewards sum to zero, so all three are zero. Combined with total mass one, this forces m_R = m_P = m_S = 1/3. Lean proves that the uniform mix is an equilibrium and that it is the unique exact equilibrium.

Worked checks

The example module uses executable #guard commands. They run during lake build.

Population (R, P, S)Best responseExploitabilityResult
(1/3, 1/3, 1/3)Rock, by tie order0Exact equilibrium
(1, 0, 0)Paper1Pure Rock can be exploited
(1/2, 3/10, 1/5)Paper3/10Accept ε = 3/10; reject ε = 1/5
(1/3, 2/3, 0)Paper, tied with Scissors—Tie order check

The uniform mix is rejected for negative ε. This case certifies best responses and equilibria in a three-action static game. It does not implement equilibrium iteration or cover dynamic MFGs.