What is a Proof?

A proof is evidence that a statement is true. In Lean, proofs are programs and statements are types. This correspondence is the foundation of everything.

The Problem: Trust

Consider this function:

1def divide (x y : Nat) : Nat := x / y

What happens when y = 0? In most languages, this crashes at runtime. You can add a comment saying "y must not be zero," but comments lie—the compiler doesn't check them.

What if the type system could guarantee that y is never zero?

1def divide (x : Nat) (y : Nat) (h : y ≠ 0) : Nat := x / y
2
3-- To call this, you must PROVE y ≠ 0
4#eval divide 10 2 (by decide)  -- Works: 5
5-- #eval divide 10 0 ???       -- Can't call! No proof possible

The parameter h : y ≠ 0 requires the caller to provideproof that y is not zero. No proof, no function call. The impossible is prevented at compile time.

Statements are Types

In Lean, mathematical statements are expressed as types:

1-- "2 + 2 = 4" is a TYPE
2#check (2 + 2 = 4)  -- Prop
3
4-- "For all natural numbers n, n + 0 = n" is a TYPE
5#check (∀ n : Nat, n + 0 = n)  -- Prop
6
7-- "There exists a natural number greater than 5" is a TYPE
8#check (∃ n : Nat, n > 5)  -- Prop

These types live in a special universe called Prop—the universe of propositions (statements that are either true or false).

Proofs are Terms

If a statement is a type, then a proof is a term of that type:

1-- The statement "2 + 2 = 4" is a type
2-- A proof of it is a term of that type
3
4example : 2 + 2 = 4 := rfl
5
6-- rfl is a proof term
7-- Its type is "2 + 2 = 4"
8-- Having such a term proves the statement

Just as 5 : Nat means "5 is a natural number," writing proof : 2 + 2 = 4 means "proof is evidence that 2 + 2 = 4."

Why Do We Need Tactics?

Proof terms can be written directly, but they get complicated fast:

1-- Direct proof term: works but unreadable
2example : ∀ n : Nat, n + 0 = n := 
3  fun n => Nat.add_zero n
4
5-- What if the proof requires many steps?
6-- The proof term becomes a nested mess of function applications

Tactics are commands that build proof terms for you. They let you describe the proof strategy in a step-by-step, human-readable way:

1-- Tactic proof: clear and structured
2example : ∀ n : Nat, n + 0 = n := by
3  intro n        -- Let n be any Nat
4  rfl            -- This is true by definition

The by keyword enters "tactic mode." Each tactic transforms the proof state until the goal is solved.

The Workflow

Proving in Lean is interactive:

1. State your goal — Write a theorem or lemma with its statement
2. Enter tactic mode — Use by
3. Read the proof state — See what you need to prove
4. Apply tactics — Transform the goal step by step
5. Close the proof — When no goals remain, you're done

A Complete Example

1-- Statement: addition is commutative
2theorem add_comm_example : ∀ a b : Nat, a + b = b + a := by
3  intro a b           -- Let a and b be any Nats
4  induction a with    -- Prove by induction on a
5  | zero => 
6    simp              -- Base case: 0 + b = b + 0
7  | succ n ih =>
8    simp [Nat.succ_add, Nat.add_succ]  -- Use known lemmas
9    exact ih          -- Apply induction hypothesis
10
11-- Now we can use this theorem
12#check add_comm_example 3 5  -- : 3 + 5 = 5 + 3

Don't worry if this looks complex—we'll build up to it step by step. The important thing is that Lean verified this proof is correct.