6. The capstone¶

We now prove the theorem the notes have been building towards: every evolutionarily stable strategy is a symmetric Nash equilibrium.

On paper the argument is three lines. Let \(x^*\) be an ESS and take any strategy \(y\). If \(y = x^*\), then \(u(y, x^*) = u(x^*, x^*)\) and there is nothing to show. Otherwise the ESS condition gives either \(u(y, x^*) < u(x^*, x^*)\) or \(u(y, x^*) = u(x^*, x^*)\), and either way \(u(y, x^*) \le u(x^*, x^*)\).

We emphasise that this argument never asks what \(u\) is. It uses only the two definitions and the fact that a strict inequality, or an equality, implies a weak one. The Lean proof has the same property, and so it holds for every game at once.

Create GameTheory/Capstone.lean, add it to GameTheory.lean, and begin:

import GameTheory.Equilibria

open Action

The statement and the proof¶

Here is the whole theorem:

/-- Every evolutionarily stable strategy is a symmetric Nash equilibrium. -/
theorem IsESS.isSymmetricNash {Strategy : Type} {payoffs : Strategy → Strategy → ℝ}
    {resident : Strategy} (stable : IsESS payoffs resident) :
    IsSymmetricNash payoffs resident := by
  intro deviation
  by_cases same : deviation = resident
  · rw [same]
  · rcases stable deviation same with worse | ⟨tie, _⟩
    · exact le_of_lt worse
    · exact le_of_eq tie

The statement reads: for any type of strategies, any payoff function and any resident strategy, given a proof stable that the resident is an ESS, the resident is a symmetric Nash equilibrium. The first three arguments are in braces, because Lean can infer them from stable. The hypothesis itself is an ordinary argument, since a proof is a value like any other.

The name IsESS.isSymmetricNash places the theorem in the IsESS namespace. We will see why that is convenient at the end of the chapter.

The goal at each step¶

At the start the context holds everything the statement introduced:

Strategy : Type
payoffs : Strategy → Strategy → ℝ
resident : Strategy
stable : IsESS payoffs resident
⊢ IsSymmetricNash payoffs resident

Compare this with every earlier proof. Here payoffs is not our Prisoner's Dilemma function but an arbitrary one, about which the context says nothing. There is no norm_num [payoff] to fall back on. Whatever we prove, we prove from stable alone.

intro deviation unfolds the Nash condition as in chapter 5, leaving:

deviation : Strategy
⊢ payoffs deviation resident ≤ payoffs resident resident

We show only the new line of the context from here on.

Two cases¶

The paper proof splits on whether the deviation is the resident itself. by_cases same : deviation = resident does exactly that. It produces two goals, one assuming the statement and one assuming its negation:

case pos
same : deviation = resident
⊢ payoffs deviation resident ≤ payoffs resident resident

case neg
same : ¬deviation = resident
⊢ payoffs deviation resident ≤ payoffs resident resident

Unlike cases in chapter 4, which split on the two constructors of Action, by_cases splits on any statement at all. Our Strategy type is arbitrary, so there are no constructors to split on, but there is always the question of whether two strategies are equal.

In the first case, rw [same] rewrites every deviation in the goal to resident. The goal becomes payoffs resident resident ≤ payoffs resident resident, and rw closes a goal that holds by reflexivity once it has finished rewriting. That single line is the "nothing to show" of the paper proof.

The hypothesis at work¶

The second case is where stable is used. stable is a proof of a ∀ followed by an implication, so as in chapter 5 we apply it like a function: first to deviation, then to same, the proof that the deviation differs from the resident. The result, stable deviation same, is a proof of the disjunction for this particular deviation.

rcases takes such a proof apart. The pattern worse | ⟨tie, _⟩ says that the disjunction has two alternatives, separated by |. The first is named worse. The second is a conjunction, whose two halves the angle brackets ⟨ ⟩, typed \< and \>, name tie and _. Two goals result:

case neg.inl
worse : payoffs deviation resident < payoffs resident resident
⊢ payoffs deviation resident ≤ payoffs resident resident

case neg.inr
tie : payoffs deviation resident = payoffs resident resident
right✝ : payoffs deviation deviation < payoffs resident deviation
⊢ payoffs deviation resident ≤ payoffs resident resident

The underscore asked Lean not to name the second half of the conjunction, and it appears in the context as right✝. The dagger marks a hypothesis we cannot refer to. An interesting observation is that this is the second-order condition of the ESS, the part that makes evolutionary stability stronger than Nash equilibrium, and the proof never needs it. The Nash property comes from the first-order condition alone, which the Lean proof makes impossible to overlook.

Each remaining goal asks for a weak inequality, and the context already contains a strict one or an equality. exact finishes a goal by supplying a proof of precisely that goal. Mathlib's le_of_lt turns a proof of a < b into a proof of a ≤ b, and le_of_eq does the same from a = b, so le_of_lt worse and le_of_eq tie are exactly what is needed.

With the cursor on the first exact, the infoview shows only the goal that its bullet is working on, case neg.inl, with worse in the context:

Those names follow the convention from chapter 3 and can often be guessed. When they cannot, the tactic exact? searches Mathlib for a lemma that closes the goal. In the first case it answers:

Try this:
  [apply] exact Std.le_of_lt worse

This is the same fact from Lean's standard library rather than Mathlib, and either works.

The theorem in use¶

The theorem is now available for any game. In particular, it gives a second proof that mutual defection is a Nash equilibrium of the Prisoner's Dilemma:

/-- Mutual defection is Nash again, this time as a consequence of stability. -/
example : IsSymmetricNash payoff defect :=
  defect_isESS.isSymmetricNash

No tactics are involved. defect_isESS from chapter 5 has type IsESS payoff defect. Because our theorem lives in the IsESS namespace, Lean lets us write defect_isESS.isSymmetricNash, finding the theorem from the type of the proof and filling in the implicit arguments. This dot notation is used throughout Mathlib, and it is why we chose the name.

We now have two proofs of the same fact. The one in chapter 5 computed the payoffs; this one uses no payoffs at all and knows only that defection is stable.

Where we are¶

We have proved that an evolutionarily stable strategy is a symmetric Nash equilibrium, for every symmetric two-player game with real payoffs. The proof is six lines, and every line corresponds to a step of the argument on paper.

Across the six chapters we have met ten tactics: norm_num, intro, cases, left, have, contradiction, by_cases, rw, rcases and exact, together with the term rfl and the combinator <;>. That is a small fraction of Lean, and it was enough to state and prove a real theorem.

Where next¶

The theorem holds for any type of strategies, and that includes mixed ones. Taking Strategy to be the probability simplex and payoffs to be the expected payoff, the result applies unchanged; the work lies in defining those two objects, not in the proof. Define expected payoffs for mixed strategies does exactly that, and Verify a mixed ESS in Hawk-Dove uses it to prove that playing hawk half the time is stable, and hence, by this chapter's theorem, a Nash equilibrium.

For game theory well beyond these notes, the elazarg/GameTheory library formalises Nash, correlated and Bayesian equilibria, sequential and repeated games, and mechanism design. Notably, it proves the existence of mixed Nash equilibria, as exists_isNash_mixed via Kakutani's fixed point theorem, and it contains its own version of this chapter's theorem. That version defines an ESS differently, with the Nash condition as its first clause, and its proof is correspondingly different. Why two equivalent definitions lead to such different proofs is discussed in Definitions and proofs.

The library is under active development, so we cite the version we read by its commit, the identifier git gives to each saved version of a project. The link 1dba332 shows the code exactly as it stood when we examined it, on 24 September 2026, even if names or proofs have changed since.