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 you'll learn about theorem proving.

Why Do We Need Proofs in Programming?

Traditional programming relies on tests to catch bugs, but tests can only check a finite number of cases. A function might work for every input you test, yet fail on some input you never considered. Proofs go further—they provideguarantees for all possible inputs.

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 safeDivide (x : Nat) (y : Nat) (h : y ≠ 0) : Nat := x / y
2
3-- To call this, you must PROVE y ≠ 0
4#eval safeDivide 10 2 (by decide)  -- Works: 5
5-- #eval safeDivide 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.

Proofs as Machine-Checked Reasoning

When you write a proof in Lean, the computer verifiesevery step. Unlike a human reviewer who might miss mistakes, Lean's kernel is extremely rigorous. If your proof compiles, it's correct—guaranteed.

1-- This proof is VERIFIED by Lean's kernel
2theorem example_proof : ∀ n : Nat, n + 0 = n := by
3  intro n
4  rfl  -- Lean checks that this step is valid
5
6-- If you try to cheat, Lean catches it:
7-- theorem bad_proof : 1 = 2 := by rfl  -- ERROR: rfl cannot prove this

This machine-checked guarantee is incredibly valuable. Mathematical papers sometimes contain subtle errors that go unnoticed for years. With Lean, such errors are caught immediately.

Statements are Types

In Lean, mathematical statements are expressed as types. This is a profound insight that connects logic and computation:

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
9
10-- Even complex statements are types
11#check (∀ a b c : Nat, (a + b) + c = a + (b + c))  -- Associativity

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. Just as 5 : Natmeans "5 is a natural number," writing proof : 2 + 2 = 4means "proof is evidence that 2 + 2 = 4."

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
9
10-- You can name proofs and reuse them
11theorem two_plus_two : 2 + 2 = 4 := rfl
12
13-- Now two_plus_two is a proof we can use elsewhere
14#check two_plus_two  -- two_plus_two : 2 + 2 = 4

The Type-Proof Correspondence

This correspondence goes deep. Consider how types and proofs relate:

When a type has no terms (like 1 = 2), it means the corresponding statement is false—there's no proof because the statement isn't true.

Prop is Not Quite Type

Propositions live in Prop rather than Type, and the difference is not cosmetic. It has one consequence you will meet constantly: proof irrelevance. Any two proofs of the same proposition are considered equal.

1-- Two different-looking proofs of the same fact
2theorem p1 : 2 + 2 = 4 := rfl
3theorem p2 : 2 + 2 = 4 := by decide
4
5-- Lean considers them the same proof:
6example : p1 = p2 := rfl
7
8-- Compare with data, where different values are genuinely different:
9-- example : (2 : Nat) = 3 := rfl   -- of course this fails

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
7-- Imagine hundreds of lines of nested lambdas and 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
5
6-- Each tactic transforms the proof state
7-- Lean constructs the underlying proof term automatically

The bykeyword enters "tactic mode." Each tactic transforms the proof state until the goal is solved. Lean then converts your tactic script into an actual proof term.

The Interactive Workflow

Proving in Lean is interactive. You write tactics one at a time, and Lean shows you the current proof state after each step:

1. State your goal — Write a theorem or lemma with its statement
2. Enter tactic mode — Use by
3. Read the proof state — The Infoview shows what you need to prove
4. Apply a tactic — Transform the goal
5. Repeat — Until all goals are solved
6. Done— When "No goals" appears, your proof is complete

1-- Watch the proof state change with each tactic
2theorem add_example (a b c : Nat) : a + b + c = c + b + a := by
3  -- Proof state: ⊢ a + b + c = c + b + a
4  omega
5  -- Proof state: No goals (proof complete!)

Common First Tactics

Here are tactics you'll use constantly:

A Complete Example

Let's trace through a complete proof to see these concepts in action:

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  -- Goal: a + b = b + a
5  induction a with    -- Prove by induction on a
6  | zero => 
7    -- Base case: 0 + b = b + 0
8    simp              -- simp knows 0 + b = b and b + 0 = b
9  | succ n ih =>
10    -- Inductive case: (n + 1) + b = b + (n + 1)
11    -- ih: n + b = b + n (induction hypothesis)
12    simp only [Nat.succ_add, Nat.add_succ]  -- simp only: plain simp loops here
13    -- Goal is now: (n + b).succ = (b + n).succ
14    rw [ih]           -- Apply induction hypothesis
15
16-- Now we can use this theorem
17#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. Every step was machine-checked.

What You'll Learn

In this section on tactics, you'll learn:

• Core tactics: rfl, rw, simp, exact, apply, intro, have
• Automation: omega, decide, aesop—tactics that solve goals automatically
• Case analysis: cases, induction, match—for breaking down problems
• Advanced techniques: calc, conv, combinators—for complex proofs
• Mathlib tactics: ring, linarith, nlinarith—powerful domain-specific tools

1example : 3 + 4 = 7 := by
2  rfl  -- Lean computes 3 + 4 = 7 and verifies it

1example (n : Nat) : n ≤ n + 1 := by
2  omega  -- omega handles linear arithmetic