Getting started

Prove 2 + 2 = 4

Compute an answer, then prove the equality.

-- #eval calculates a value. It prints 4.
#eval 2 + 2

-- theorem names a proof; : introduces its proposition.
-- Lean infers Nat (natural numbers) for these numerals.
theorem two_plus_two : 2 + 2 = 4 := by
  rfl

-- rfl stands for reflexivity: an expression equals itself.
-- Both sides reduce to 4, so Lean accepts the proof.
-- Change 4 to 5 above and check the file to see an error.

-- Reuse the named proof as a term of the required type.
example : 2 + 2 = 4 := two_plus_two

Explanation

`#eval`

Executes an expression and displays its value. Evaluating 2 + 2 and proving an equality are separate commands.

`theorem … : … := …`

Gives a proof a name, states the proposition after :, and supplies the proof after :=.

`by rfl`

Starts a tactic proof and uses reflexivity. Lean checks that the two sides reduce to the same expression.

Expected output

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

Exercise

Add a named proof that 3 + 3 = 6. Then try an incorrect result and read the diagnostic.