Lean: When Theorems Become Code

Lean is a programming language with an unusual primary audience: mathematicians. It’s designed to formalize mathematics, letting mathematicians treat their field like software engineering—breaking proofs into structures, importing each other’s theorems, and versioning them on GitHub. The goal is to eventually make much of humanity’s mathematical knowledge statically checked, verifiable, and composable.

What does it feel like to work in Lean? Let’s start with the basics.

The Anatomy of a Proof

Here’s a tiny theorem stating that 2 equals 2:

theorem two_eq_two : 2 = 2 := by
  sorry

On the surface, this looks like a mathematical statement: we have the theorem keyword, a name, a colon, the statement to prove, and the proof following := by. But if you’re a programmer, something looks off. The theorem resembles a function definition, which would make 2 = 2 its return type. How can an equality be a type? And if it is a type, what are its values? These are deep questions we’ll set aside for now.

Let’s inspect the proof instead:

theorem two_eq_two : 2 = 2 := by
  sorry

Place your cursor just before the sorry and check the “Tactic state” panel on the right. You’ll see:

Goal is 2 = 2

The ⊢ symbol denotes the goal—the statement you must prove. Here, it’s 2 = 2. Move the cursor past the sorry:

No goals

The goal vanishes. In effect, sorry acts as a universal proof, closing any goal. It’s a placeholder (or a lie) that suppresses the checker—much like any in TypeScript lets you bypass type checking without proving anything useful. Remove it:

Now the proof is incomplete and the goal unsolved. To finish it, use rfl, short for “reflexivity,” which closes goals shaped like something = something:

Once the goal is closed, the theorem is complete:

theorem two_eq_two : 2 = 2 := by
  rfl

You can now reference this fact elsewhere:

theorem two_eq_two : 2 = 2 := by
  rfl
 
theorem two_eq_two_again : 2 = 2 := by
  exact two_eq_two

Here, two_eq_two_again delegates to the earlier theorem because its goal is exactly what two_eq_two proves. To a programmer, this looks like returning the result of a function call. The commands exact, sorry, and rfl are called tactics—each used to close different kinds of goals.

Math You Can Break

Proving 2 = 2 is trivial. What about 2 = 3?

theorem two_eq_two : 2 = 2 := by
  rfl
 
theorem two_eq_three : 2 = 3 := by
  sorry

Unsurprisingly, sorry can close this too:

But that’s cheating. Replace it with rfl:

It fails. rfl only handles goals where both sides are literally identical. This is a good thing—in standard mathematics, 2 = 3 is false and shouldn’t be provable.

Yet mathematics isn’t set in stone. You can define your own “haunted” mathematical universe. Declaring an axiom takes a statement on faith:

axiom math_is_haunted : 2 = 3

This is equivalent to theorem math_is_haunted : 2 = 3 := by sorry, but without the apology. With this axiom available, proving 2 = 3 becomes straightforward:

theorem two_eq_two : 2 = 2 := by
  rfl
 
axiom math_is_haunted : 2 = 3
 
theorem two_eq_three : 2 = 3 := by
  exact math_is_haunted

Lean accepts this without complaint. More sinister consequences follow. Let’s prove 2 + 2 = 6:

theorem two_eq_two : 2 = 2 := by
  rfl
 
axiom math_is_haunted : 2 = 3
 
theorem two_add_two_eq_six : 2 + 2 = 6 := by
  -- We'll write something here (this is a comment, btw)

The initial goal is ⊢ 2 + 2 = 6:

No tactic directly solves it, but math_is_haunted gives us a proof that 2 = 3. If 2 is the same as 3, then proving 3 + 3 = 6 should suffice. The rewrite tactic performs exactly this substitution, like a find-and-replace within the goal:

Now the goal is ⊢ 3 + 3 = 6, which rfl closes:

theorem two_eq_two : 2 = 2 := by
  rfl
 
axiom math_is_haunted : 2 = 3
 
theorem two_add_two_eq_six : 2 + 2 = 6 := by
  rewrite [math_is_haunted]
  rfl

Technically, rfl succeeds here by unfolding the definitions of 3, 6, and + until both sides reduce to identical Peano representations (Nat.zero.succ.succ...), making it a genuine something = something case.

This is unsettling in a useful way. The math_is_haunted axiom lets us derive a contradiction (e.g., both 2 + 2 = 6 and 2 + 2 ≠ 6), and from a contradiction, logic allows proving anything. While this was deliberate on our part, a similar incident actually struck mathematics in the early 20th century when Russell’s paradox exposed a contradiction in Set Theory’s axioms—prompting a lengthy patch-up.

Delete the bad axiom and the proof breaks:

Good—broken things shouldn’t check. Fix the statement to a true one:

With the bad axiom gone, math is sane again.

This illustrates the core of proof checking: Lean validates that conclusions follow logically from chosen axioms. It doesn’t care about truth in an absolute sense; it verifies consistency. If the axioms are sound and the tool is sound, the derived theorems are sound—whether the proof is one rfl or millions of lines.

Formalizing 100 Pages of Math

Consider Fermat’s Last Theorem: for any n greater than 2, no positive naturals x, y, and z satisfy xⁿ + yⁿ = zⁿ.

import Mathlib
 
theorem PNat.pow_add_pow_ne_pow (x y z : ℕ+) (n : ℕ) (hn : n > 2) :
    x^n + y^n ≠ z^n := by
  sorry

Proven in 1994 after 350 years, the proof spans over 100 pages. An ongoing project aims to formalize it in Lean—an effort expected to take years. Opening the current FermatsLastTheorem.lean reveals a proof that still relies on sorrys:

#print axioms PNat.pow_add_pow_ne_pow
/-
'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
-/

When complete, none of the dependencies will contain sorry, and #print axioms PNat.pow_add_pow_ne_pow will no longer list sorryAx. For mathematicians and programmers alike, that merge request will be exceptionally satisfying.

Getting Started

Today’s examples didn’t prove anything useful, but the experience offers a glimpse of something distinctive—part programming, part logic, entirely absorbing. If you’re curious:

  • The Natural Numbers Game offers a gentle, fun introduction and reveals what natural numbers are built from.
  • Early chapters of Mathematics in Lean assume no math background and are useful for learning basic tactics.
  • Tao’s Analysis has a Lean companion, actively developed on GitHub.
  • The “new members” channel on the Lean Zulip instance is welcoming to beginners.

Lean combines ideas from both mathematics and programming in surprising, mind-bending ways. For a certain kind of person, it’s just fun—and worth trying for no particular reason at all.