Your first checked statement
Read a claim, write rfl, and let Lean check it.
Your first proof takes a minute. Type rfl below the statement and press Check. Lean replies in a second or two; no account needed.
In this course 1 / 11
Lean is a programming language that can also check claims. You write a claim, write a proof, and Lean either accepts the proof or tells you exactly what is wrong. Here is a complete claim with its proof:
example : 2 + 3 = 5 := by
rflRead it in three parts. example : starts a claim. 2 + 3 = 5 is the claim itself. := by starts the proof, and the indented line under it is the proof: one tactic, an instruction to Lean.
rfl says: compute both sides and see that they are the same. Lean works out 2 + 3, gets 5, compares it with the right side, and accepts. A theorem is the same thing with a name, so it can be used again later: theorem five : 2 + 3 = 5 := by rfl.
In the exercise the claim is already written. You only write the proof underneath it and press Check.
Worked example
example : 2 + 3 = 5 := by
rfl
theorem ten : (2 + 3) * 2 = 10 := by
rfl
At the start of the proof on line 1. Everything above ⊢ may be used; the line below it is what must be proved.
The second claim has a name, ten. Both sides still compute to the same number, so the same tactic works.
A claim goes after the colon, its proof after := by. rfl proves an equation whose two sides compute to the same value.
Prove that four plus four equals eight.
Suggested steps
- Write the tactic that computes both sides
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