Lean 4 Formal Verification Basics¶

What is Lean 4?¶

Lean 4 is a theorem prover and programming language developed by Microsoft Research. It allows you to write mathematical proofs that are mechanically verified.

Basic Syntax¶

Defining Functions¶

def double (n : Nat) : Nat := n * 2

#eval double 5  -- Output: 10

Propositions and Proofs¶

theorem add_zero (n : Nat) : n + 0 = n := by
  rfl  -- reflexivity

theorem add_succ (n m : Nat) : n + Nat.succ m = Nat.succ (n + m) := by
  rfl

Common Tactics¶

Example: Proving Commutativity¶

theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ n ih => simp [Nat.succ_add, ih]

Resources¶

• Lean 4 Documentation
• Mathematics in Lean
• Theorem Proving in Lean 4

Practice Problems¶

1. Prove 0 + n = n
2. Prove (a + b) + c = a + (b + c) (associativity)
3. Prove a * 1 = a (multiplicative identity)