Read Lean’s reply
The four replies you will see most, word for word, and what to do about each.
In this course 3 / 11
Every Check gets a reply from Lean. Most of learning Lean is reading that reply calmly, so here are the four you will see most often, exactly as Lean prints them.
1. Accepted. The Goal tab says No goals left. There is nothing more to do.
2. A name Lean does not know. Usually a typo. In a proof, Lean says unknown tactic:
example : 2 + 3 = 5 := by
rlfunknown tactic
Elsewhere it names the word it could not find: Unknown identifier dobule. The editor often catches typos before you spend a check and suggests the closest word it knows.
3. The claim is false. rfl shows the two sides it computed. If they differ, the claim is wrong, not the tactic:
example : 2 + 3 = 6 := by
rflTactic `rfl` failed: The left-hand side 2 + 3 is not definitionally equal to the right-hand side 6
4. Unsolved goals. Every step worked, but the proof is not finished. Lean prints what is still left to prove after the symbol ⊢. You will meet this one constantly from the next course on, and it is good news: it tells you the next thing to do.
One rule for all of them: read the first error, fix only that, and check again. A single mistake often causes a second error further down, and that one disappears with the first.
Worked example
-- Fix 1: the tactic is spelled rfl.
example : 2 + 3 = 5 := by
rfl
-- Fix 2: the claim said 6, but two plus three is five.
example : 2 + 3 = 5 := by
rfl
At the start of the proof on line 2. Everything above ⊢ may be used; the line below it is what must be proved.
Both fixes were small: correct one spelling, or correct one number in the claim. The reply told you which.
Read Lean’s first reply before changing anything. An unknown name is a spelling problem, a failed rfl shows the two sides it compared, and unsolved goals show what is left.
This proof has a typo. Read the reply under the editor and fix the spelling.
Suggested steps
- Correct the spelling of the tactic
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct