Foundations · 4 min
Prove 2 + 2 = 4
Start with a fact you already know: 2 + 2 = 4. #eval 2 + 2 computes the answer. A theorem declaration also states an equality and asks Lean to check evidence for it.
Read theorem four : 2 + 2 = 4 := by as “define a proof named four of the proposition 2 + 2 = 4, using these tactics.” Here the numerals have type Nat, the natural numbers.
rfl stands for reflexivity: an expression equals itself. Lean reduces both sides to 4, so rfl proves this equality. It does not prove every true equation.
sorry marks a missing proof. Lean issues a warning, and this lesson remains unfinished until you replace it. After completing the proof, try changing 4 to 5 and read the error.
Exercise
Replace sorry with rfl to prove 2 + 2 = 4.
Open exercise in editor#eval 2 + 2
theorem four : 2 + 2 = 4 := by
sorry
Hint
rfl works because both sides reduce to the same natural number.
Solution
#eval 2 + 2
theorem four : 2 + 2 = 4 := by
rfl