Writing Your First Proofs in Lean

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

• intro hA moves the first assumption from the goal into the local context
• intro _hB moves the second
• exact hA closes the goal with a term already in scope

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:

• Cleaner syntax. fun hA => hA instead of Lam("x", A, Var("x")).
• Tactics. intro, exact, apply let you construct proofs step by step instead of writing the whole term at once.
• Backwards reasoning. apply lets you work from the goal toward the hypotheses, which is often more natural than forward construction.

#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 but 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:

• the zero case
• the succ case, where you get an induction hypothesis ih

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

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

• In the Python article, we could not do induction at all. The prover only handled propositional logic.
• In the Julia article, induction looked like recursion over Nat types, and every step was a manual axiom chain.
• In Lean, induction is a built-in tactic, and simp handles the routine cases. The same idea, but with the mechanical drudgery removed.

#What Makes Lean Feel Different from Programming

Working in Lean is less like writing code and more like steering toward a target the tool keeps in front of you. The goal is always visible: you are trying to inhabit one specific type, and at every step Lean prints what remains to prove. The hypotheses in scope usually matter more than the order of commands you typed. And the high-level tactics, rfl, rw, simp, induction, all bottom out in a proof term checked against a small kernel, the same architecture as the Python and Julia provers earlier in this series, with far better tooling on top. The mental shift is from tracing how code runs to asking what would count as evidence that a statement holds.

#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:

• This is an implication, so I probably need intro
• After two intros, I should have A in the context
• Then exact that hypothesis

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:

• cases for splitting on inductive data
• constructor for building structured proofs
• have for introducing intermediate lemmas
• apply for working backwards from the goal
• omega for automatically solving linear arithmetic
• simp and rw well enough that arithmetic proofs stop feeling manual

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.