Definitions and proofs¶

In formalisation, the definitions are usually harder than the proofs. This claim, made in chapter 2 of the tutorial, is easy to state and hard to believe until it has been seen. The evolutionarily stable strategy gives a clean example. Two textbook definitions of an ESS are provably equivalent, yet under one of them the theorem of chapter 6 takes six lines and under the other it takes a single word.

Two definitions of the same thing¶

The tutorial defines an ESS as follows. A strategy \(x^*\) is evolutionarily stable if every distinct mutant \(y\) either does strictly worse against it, or ties against it and then does strictly worse against itself:

In Lean, from chapter 5:

def IsESS {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
    (resident : Strategy) : Prop :=
  ∀ mutant : Strategy, mutant ≠ resident →
    payoffs mutant resident < payoffs resident resident ∨
      (payoffs mutant resident = payoffs resident resident ∧
        payoffs mutant mutant < payoffs resident mutant)

Many textbooks instead split the condition into two clauses. The first says that \(x^*\) is a best reply to itself; the second applies only to mutants that tie:

This is the form used by the elazarg/GameTheory library, in GameTheory/Evolutionary/Basic.lean, in the version we examined, commit 1dba332. A commit is one saved version of a project's history, and citing it pins the code we quote even if the library later changes. Adapted to our names and argument order, it reads:

def IsESSNashFirst {Strategy : Type} (payoffs : Strategy → Strategy → ℝ)
    (resident : Strategy) : Prop :=
  (∀ mutant : Strategy, payoffs mutant resident ≤ payoffs resident resident) ∧
    ∀ mutant : Strategy, mutant ≠ resident →
      payoffs mutant resident = payoffs resident resident →
        payoffs mutant mutant < payoffs resident mutant

The same theorem, twice¶

Under the second definition, the first clause is word for word the Nash condition of chapter 5. The theorem that an ESS is a symmetric Nash equilibrium therefore needs no argument at all:

theorem IsESSNashFirst.isSymmetricNash {Strategy : Type}
    {payoffs : Strategy → Strategy → ℝ} {resident : Strategy}
    (stable : IsESSNashFirst payoffs resident) :
    IsSymmetricNash payoffs resident :=
  stable.1

stable.1 is the first half of the conjunction. Compared with the six-line proof of chapter 6, with its case split and its two Mathlib lemmas, it is tempting to conclude that the second definition is simply better. That conclusion is premature.

Where the work went¶

The two definitions are equivalent, and Lean can confirm it:

/-- The two definitions of evolutionary stability agree. -/
theorem isESS_iff_isESSNashFirst {Strategy : Type}
    {payoffs : Strategy → Strategy → ℝ} {resident : Strategy} :
    IsESS payoffs resident ↔ IsESSNashFirst payoffs resident := by
  constructor
  · intro stable
    refine ⟨stable.isSymmetricNash, ?_⟩
    intro mutant distinct tie
    rcases stable mutant distinct with worse | ⟨_, second⟩
    · exact absurd tie (ne_of_lt worse)
    · exact second
  · intro stable mutant distinct
    rcases lt_or_eq_of_le (stable.1 mutant) with worse | tie
    · exact Or.inl worse
    · exact Or.inr ⟨tie, stable.2 mutant distinct tie⟩

The proof uses a few tactics beyond the tutorial, but its shape is what matters. constructor splits the ↔ into its two directions.

The first direction, from our definition to the other one, has to produce the Nash clause. It does so by calling stable.isSymmetricNash, which is the theorem of chapter 6 itself. The second direction runs the same argument backwards: lt_or_eq_of_le splits a weak inequality into a strict one or an equality, which is the case split of chapter 6 reversed.

In other words, the reasoning of chapter 6 has not been avoided. It has moved out of the theorem and into the claim that the definition is the right one. Anyone who adopts the second definition either proves an equivalence like this, or takes on trust that the two clauses capture Maynard Smith and Price. Lean does not help with the second option. It checks that a definition is well formed, and never that it means what we intended.

What Lean cannot check¶

Chapter 5 gave the sharpest example of this. Remove the hypothesis mutant ≠ resident from our definition and the resident becomes its own mutant, so the definition demands payoffs resident resident < payoffs resident resident in one form or another. No strategy satisfies it. Lean accepts that definition without a word, because it is a perfectly good statement that happens to hold of nothing, and every theorem of the form 'if \(x^*\) is an ESS then ...' becomes true for the wrong reason.

A proof, by contrast, is checked completely. If the six lines of chapter 6 compile, the theorem holds for the definitions as written. The risk in a formalisation therefore sits almost entirely in the definitions, and the best available defence is the one used above: prove that the definition agrees with an independent formulation, or check it against examples where the answer is known, as chapter 5 did with the Prisoner's Dilemma.

The choice between them¶

Neither definition is wrong, and the choice depends on what the definition is for. A library wants the form that makes downstream use easy. The Nash-first form hands every user the most commonly needed consequence for free, and in elazarg/GameTheory the few lines of IsESS.isNash_symmetric are spent translating into the library's general notion of Nash equilibrium for any number of players, not on game theory. Teaching notes want the form closest to how the reader first met the concept, so that the proof reproduces the argument the reader already knows.

We chose the disjunctive form for the tutorial for that second reason. The equivalence above is what makes the choice safe: whichever definition a reader prefers, the theorem holds for both.