Proofs

Your first proof

A theorem is a declaration whose type is a proposition. Lean checks the supplied proof.

-- Two sides that compute to the same value
theorem two_plus_two : 2 + 2 = 4 := by
  rfl

-- A statement about every natural number
theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

#check two_plus_two
#check add_zero

Explanation

`theorem`

Introduces a named proposition together with its proof.

`by`

Begins a tactic proof. Tactics construct a proof term that Lean checks.

`rfl`

Short for reflexivity: a value equals itself. It proves equality when Lean can reduce both sides to the same expression.

Expected output

Reference only. Run the file to check its actual result.

two_plus_two : 2 + 2 = 4
add_zero (n : Nat) : n + 0 = n

Exercise

Change 4 to 5 and check the file. Read why rfl cannot finish the proof.