Writing Your First Proofs in Lean

7 min read Keywords:  lean, theorem proving, formal verification, tactics, induction, lean 4
A kneeling figure watches in awe as a glowing substance emerges from an experiment in a dark vaulted laboratory
The Alchymist, Joseph Wright of Derby, 1771

The first article in this series explained the Curry-Howard correspondence: propositions are types, proofs are programs. The second built a tiny theorem prover from scratch in Python. The third embedded the same ideas inside Julia’s type system.

Now we use the real tool. This article takes the exact same theorems you proved by hand in Python and shows them in Lean 4. You will see what changes and what stays the same: the syntax shifts, the logic does not.

#The Same Three Theorems

In the Python article, we proved three things:

  1. A -> A (if A then A)
  2. A -> B -> A (if A and B, then A)
  3. (A -> B) -> (B -> C) -> A -> C (composition of implications)

We built each proof as a lambda term and fed it to a 30-line type checker. If the checker accepted the term, the proof was valid.

Lean works the same way. The difference is that Lean’s kernel is much more powerful, and there are layers of automation on top. But underneath, it is still: construct a term, check its type.

#Proof 1: A -> A

In Python, the proof was:

identity = Lam("x", A, Var("x"))
# inferred type: Arrow(Atom("A"), Atom("A"))

In Lean:

theorem identity (A : Prop) : A -> A :=
  fun hA => hA

Same structure. fun hA => hA is a lambda that takes evidence of A and returns it. The type A -> A is both the function signature and the logical claim. The term is both the program and the proof.

In the Python prover, we had to call infer({}, identity) to check the proof. In Lean, writing theorem triggers the type checker automatically. If the term does not inhabit the claimed type, the file does not compile.

#Proof 2: A -> B -> A

In Python:

proof = Lam("x", A, Lam("y", B, Var("x")))
# inferred type: Arrow(A, Arrow(B, A))

In Lean:

theorem keep_first (A B : Prop) : A -> B -> A :=
  fun hA _hB => hA

Ignore the second assumption, return the first. The proof term is identical in structure to the Python version. The only difference is syntax: fun instead of Lam, => instead of a comma, underscores for unused bindings.

The same proof as a tactic proof:

theorem keep_first_tac (A B : Prop) : A -> B -> A := by
  intro hA
  intro _hB
  exact hA

The Python prover has no tactic system. You write the proof term or you write nothing. Lean gives you both options: write the term directly, or use tactics to construct it step by step. Tactics scale to longer proofs in ways that term construction does not.

#Proof 3: (A -> B) -> (B -> C) -> A -> C

This was the most complex proof in the Python article:

compose = Lam(
    "f", Arrow(A, B),
    Lam(
        "g", Arrow(B, C),
        Lam(
            "x", A,
            App(Var("g"), App(Var("f"), Var("x")))
        )
    )
)

In Lean:

theorem compose (A B C : Prop) : (A -> B) -> (B -> C) -> A -> C :=
  fun hAB hBC hA => hBC (hAB hA)

Function application in Lean is just juxtaposition: hAB hA applies hAB to hA. No App(Var("f"), Var("x")) wrapper needed. The proof is a one-liner instead of a nested tree.

The tactic version:

theorem compose_tac (A B C : Prop) : (A -> B) -> (B -> C) -> A -> C := by
  intro hAB hBC hA
  apply hBC
  apply hAB
  exact hA

Here apply works backwards from the goal. The goal is C. apply hBC says “I have B -> C, so if I can prove B, I’m done.” Now the goal becomes B. apply hAB says “I have A -> B, so if I can prove A, I’m done.” Now the goal becomes A. exact hA closes it.

Working backwards from the goal is a tactic idiom that has no analog in the Python prover. It is one of the things that makes Lean proofs more natural than raw term construction.

#What You Just Saw

You proved three theorems in two systems. The logic is the same. The checker is the same kind of machine. But Lean gives you:

#Beyond Implication: Equality and Computation

The Python prover handles only implication. It cannot talk about equality, numbers, or computation inside types. Lean can.

theorem one_plus_one : 1 + 1 = 2 := by
  rfl

rfl means reflexivity: both sides reduce to the same normal form, so equality holds by computation. Lean evaluates 1 + 1 to 2, sees that both sides are identical, and closes the goal.

This is one of the most important ideas in Lean. A lot of proving is not deep reasoning. It is getting both sides of a statement into forms that Lean’s reduction machinery can recognize as equal. In the Julia article, proving 1 + 1 = 2 took four steps of manual axiom chaining. In Lean, rfl triggers the kernel’s reduction and closes the goal.

#Rewriting

When rfl is not enough, you can rewrite one equality into another.

theorem add_zero_twice (n : Nat) : (n + 0) + 0 = n := by
  rw [Nat.add_zero]

rw means: use an equality as a rewrite rule. Nat.add_zero is the lemma that n + 0 = n. Lean applies it to all matching subterms in the goal, closing it in one step.

This is where Lean starts to feel less like programming and more like symbolic transformation. You apply proven equalities to transform the goal.

#Simplification

Repeated rewriting gets tedious. simp is Lean’s general-purpose simplifier.

theorem add_zero_twice_simp (n : Nat) : (n + 0) + 0 = n := by
  simp

simp applies a large collection of known simplification lemmas automatically. This is the first point where the gap between a toy prover and Lean becomes unmistakable. In the Python prover, you do everything by hand. In the Julia article, every step is a manual axiom chain. In Lean, simp handles the routine work.

#Induction

For properties that hold for all natural numbers, you need induction.

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero =>
      rfl
  | succ n ih =>
      simp

induction n with splits the proof into:

That is mathematical induction in executable form: base case, then inductive step.

This is the moment where the earlier articles should click together:

#What Makes Lean Feel Different from Programming

Three things:

  1. The goal is always visible. You are not just writing code. You are trying to inhabit one specific type. At every step, Lean shows you what remains to be proved.

  2. Context matters more than control flow. The local hypotheses in scope often matter more than the sequence of commands you typed.

  3. Automation is layered on top of a tiny core. rfl, rw, simp, and induction feel high-level, but underneath Lean is still checking a proof term against a small kernel. The same architecture as the Python and Julia provers, just with much better tooling.

Lean feels alien because ordinary programming trains execution thinking. Lean trains you to think in terms of evidence.

#A Good Way to Learn

Learn Lean by reading goals, not by memorizing tactics.

  1. Look at the goal.
  2. Ask what shape of term would inhabit it.
  3. Use tactics only to help construct that term.

So when you see:

⊢ A -> B -> A

you should think:

You already know this from the Python article. The proof term is fun hA _hB => hA. The tactics are just an interface for building that same term incrementally.

#Where to Go Next

After these first proofs, the next things worth learning are:

At that point Lean becomes pleasant to use.

Once you see proofs as typed constructions rather than ceremony, Lean’s tactics become predictable. And if you have followed this series from the beginning, you already have that mental model. The Python prover gave you the architecture. The Julia prover gave you the trust boundary. Lean gives you the automation to work at scale.

The difficulty is the same as programming: details require precision.