Read an error message¶

Lean's error messages are precise but not always friendly. This page lists the errors met most often when writing game theory in Lean, each with the message as Lean prints it, what it means, and the usual fix. The position before each message, such as 12:10, is the line and column where Lean reports the problem.

unsolved goals¶

This is the most common error of all:

error: GameTheory/Probe.lean:9:41: unsolved goals
⊢ payoff defect cooperate = 5

The tactics ran without failing but did not finish the proof, and what is left is shown after the ⊢. The position points at the by, not at the line where something is missing. The usual fix is another tactic, or a hint to an existing one: this message came from norm_num without [payoff].

unsolved goals and a missing import¶

Sometimes the goal left over looks too simple to have been missed:

error: GameTheory/Probe2.lean:3:25: unsolved goals
⊢ 3 < 5

When a goal as simple as 3 < 5 is left unsolved, the tactic is missing part of itself. This came from a file importing only Mathlib.Data.Real.Basic, where norm_num exists but its extensions for inequalities do not. Adding import Mathlib.Tactic.NormNum fixes it. A missing import rarely produces an error that mentions imports.

Unknown identifier¶

A misspelt name produces:

error: GameTheory/Probe.lean:12:10: Unknown identifier `payof`

A name Lean does not know: usually a typo, a missing import, or a namespace that has not been opened. Here it was a typo for payoff. The same line also produces a second, confusing error, ⊢ sorry () = 5, because Lean carries on with a placeholder, sorry, in place of the unknown name. Fix the first error and the second disappears.

Ambiguous term¶

A name defined in two places produces:

error: GameTheory/HowTo/EveryStrategy.lean:12:45: Ambiguous term
  payoff
Possible interpretations:
  _root_.payoff : Action → Action → ℝ

  RockPaperScissors.payoff : Hand → Hand → ℝ

Two definitions with the same name are both visible, here the Prisoner's Dilemma payoff and the one opened from RockPaperScissors. Write the full name, RockPaperScissors.payoff, or work inside the namespace rather than opening it. See Encode a new game.

Missing cases¶

A payoff matrix with cells left out produces:

error: GameTheory/Probe.lean:16:2: Missing cases:
cooperate, defect
defect, cooperate

A definition by cases leaves some inputs uncovered, here two cells of a payoff matrix. The message lists exactly which, so add a line for each.

Type mismatch¶

A proof of the wrong statement produces:

error: GameTheory/Probe.lean:23:2: Type mismatch
  smaller
has type
  a < b
but is expected to have type
  a ≤ b

A proof was given for a different statement from the goal. Lean does not convert between < and ≤, or between other close relatives, on its own. Bridge the gap with a lemma, here exact le_of_lt smaller. See Find a lemma.

linarith failed¶

When linarith cannot find its argument, it shows what it tried:

error: GameTheory/Probe.lean:20:2: linarith failed to find a contradiction
x : ℝ
positive : 0 < x
a✝ : 0 ≤ x
⊢ False
failed

linarith works by assuming the goal is false and deriving a contradiction, which is why the negated goal appears as a✝. Failure means that no linear combination of the hypotheses works. Either the statement is false, as it is here, or a definition needs unfolding first, or the argument needs products, in which case try nlinarith. See Prove an inequality.

There are no additional binders¶

A tactic applied to a goal of the wrong shape produces messages such as:

error: GameTheory/Probe.lean:26:8: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

⊢ payoff cooperate defect < payoff defect defect

intro was used on a goal that does not begin with ∀, → or ¬. Look at the goal and choose a tactic that fits its shape.

Invalid field¶

Dot notation on a theorem that cannot be found produces:

error: GameTheory/HowTo/MixedPayoff.lean:22:9: Invalid field `isSymmetricNash`: The environment does not contain `Function.isSymmetricNash`, so it is not possible to project the field `isSymmetricNash` from an expression

stable.isSymmetricNash asks for the theorem IsESS.isSymmetricNash, since stable is a proof of an IsESS statement. When that theorem is not available, Lean unfolds IsESS to the ∀ underneath and tries again under the name Function, which is what the message reports. The usual cause is a missing import, here of GameTheory.Capstone, or a misspelt theorem name.

decide failed¶

decide fails on any statement about real numbers, with a long message ending in Classical.choice. This is not a bug in the proof; see Computation and the real numbers.