Your first checked statement
Read a theorem, write rfl, and check a proof of a calculation.
Your first proof takes a minute. Type rfl below the statement and press Check. Lean checks it in a second or two; no account needed.
In this course 1 / 14
Lean checks mathematical claims using proofs you write. A claim might say that a calculation gives a particular answer, or that a property holds for every input of a function. We will start with a calculation.
Read example : 2 + 3 = 5 := by as “prove that two plus three equals five”. The colon starts the claim. The words := by start its proof. The indented line below contains a tactic: an instruction that builds part of the proof.
rfl proves an equality when both sides become the same expression by computation. For 2 + 3 = 5, Lean computes the left side to 5. The two sides agree, so the proof is complete.
In the exercise, the statement is already written. Write the proof in the editable area and press Check. The goal is the statement after ⊢; when Lean accepts the proof, no goals remain. You can check right away, without an account.
Worked example
example : 2 + 3 = 5 := by
rfl
example : (2 + 3) * 2 = 10 := by
rflThe second proof computes a sum and then a product. The same tactic works because both sides reduce to the same number.
Read the statement first. Write a proof below by, then check it. rfl is enough when both sides compute to the same expression.
Prove that four plus four equals eight. Enter one tactic below the statement.
Suggested steps
- Let both sides reduce to the same number
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