By David Monaghan & Claude Sonnet 5.5

I installed Lean on 1 November and decided to use it on as many of my projects as I can. In three days it found real bugs in four of them. This post is what I'd have wanted to read before I started.

It's written for someone who already writes tests and ships production code, in TypeScript or Rust or anything else, and has no background in proofs. By the end you'll have run a small example that finds a bug, seen how to check that a proof describes your real code, and have a rule for what's worth proving. I'm three days in, so treat it as a field report and not a course.

Tests check the cases you thought of

A test runs your code on inputs you chose. If your tests pass and a user then does something nobody tried, the tests had nothing to say about it.

Lean is a programming language that can check an argument about every input. You write a claim about your code, then the steps that show it's true, and Lean checks every step. If one is wrong, it won't compile. That makes a proof a test for all the cases, with one catch that matters a lot: a proof is about a model of your code, written in Lean, not about your TypeScript or Rust directly.

So the working method has two jobs, and the rest of this post follows them:

Prove the claim about the model.
Check that the model and the real code agree.

The whole method, in one picture

An animated diagram in two lanes. Lane one: a claim goes into Lean, which answers that it cannot prove it and shows a counterexample of three conflict failures in a row where nobody is told. After the rule is fixed, Lean answers proved. Lane two: the same inputs go into the real code and the Lean model, and their answers are compared. With the old rule 140 answers differ. With the fixed rule all 511 agree. — The two jobs. Top: a claim fails with a counterexample, the rule is fixed, and the proof goes through. Bottom: the same inputs go through the real code and the model, and the answers are compared.

The numbers in that picture are real. They come from the example below, which you can run.

Install it in a few minutes

The installer is called elan. It's the Lean equivalent of rustup or nvm.

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
lean --version

That's enough for everything here. The examples use only Lean's core library, no add-on packages, so each one compiles in about a second. I ran them on Lean 4.35. For an editor, the "Lean 4" extension for VS Code shows you the goal you still have to prove as you type, which is the best way to learn what's going on.

If you later add Mathlib, the big maths library, one habit will save you a lot of time: run files with lake env lean --run file.lean, not lake exe. A lake exe build of anything that imports Mathlib compiles all of Mathlib first, which takes minutes and gigabytes. I found that out on day one.

A bug you can reproduce: the retry counter

Here's a simplified version of a rule from a job runner I wrote. When a job fails, count the failure. After 3 failures in a row, tell a human. The rule is short, and the comment above it in my code said it clearly: the third strike always reaches a person, whatever the cause.

Here is that rule as a Lean model, with the bug in it. Put it in a file called Retry.lean.

/-- Why a job failed. Only the merge-conflict case is special. -/
inductive Cause where
  | conflict
  | other

/-- After this many failures in a row, a human is told. -/
def limit : Nat := 3

/-- The streak counter after one more failure. THE BUG: on a conflict, the
    counter is reset just before it would reach the limit. -/
def stepBuggy (n : Nat) : Cause → Nat
  | .conflict => if n + 1 ≥ limit then 0 else n + 1
  | .other    => n + 1

/-- The fix: every failure adds one. -/
def stepFixed (n : Nat) (_ : Cause) : Nat := n + 1

/-- Does a run of failures reach a human? Start with streak `n`. -/
def pages (step : Nat → Cause → Nat) : Nat → List Cause → Bool
  | _, []      => false
  | n, c :: cs => decide (step n c ≥ limit) || pages step (step n c) cs

-- Try the claim: three conflicts in a row.
#eval pages stepBuggy 0 [.conflict, .conflict, .conflict]   -- false: nobody is told
#eval pages stepFixed 0 [.conflict, .conflict, .conflict]   -- true

Run it with lean Retry.lean and Lean prints false, then true.

That's the bug. With the buggy rule, three merge conflicts in a row never reach a person. The counter goes 1, 2, back to 0, and starts again, so every lap costs a paid job and nobody is ever told. A test that tried a few failures in a row would likely have used other and passed.

A few things to know if the syntax is new. inductive defines a type with a fixed set of cases. def defines a function, and the | lines are pattern matches, like a switch that the compiler checks is complete. #eval runs an expression and prints the result. Everything here is pure data in and data out, which is exactly what makes it provable.

Proving the fix

The claim, in plain words: any run of at least 3 failures reaches a human, whatever the causes. In Lean:

theorem fixed_pages (cs : List Cause) (h : limit ≤ cs.length) :
    pages stepFixed 0 cs = true := by
  have key : ∀ (cs : List Cause) (n : Nat),
      limit ≤ n + cs.length → 0 < cs.length → pages stepFixed n cs = true := by
    intro cs
    induction cs with
    | nil => intro n _ h; simp at h
    | cons c cs ih =>
      intro n h _
      simp only [pages, stepFixed]
      by_cases hn : n + 1 ≥ limit
      · simp [hn]
      · have : 0 < cs.length := by simp [limit] at *; omega
        have := ih (n + 1) (by simp at h; omega) this
        simp [this]
  exact key cs 0 (by simpa using h) (by simp [limit] at h; omega)

Add that under the first block and run lean Retry.lean again. If it compiles with no errors, the claim is proved for every list of causes of any length.

You do not need to follow that proof line by line, and I don't write proofs like this by hand. A coding agent writes the model and the proofs for me, and Lean is the part I don't have to trust, because it checks every step. What I do read is the statement, and it has three parts:

The name after theorem says what it's about.
Everything before the colon is what you assume: a list of causes cs, and h, that it has at least limit entries.
Everything after the colon is what Lean has proved: pages stepFixed 0 cs = true.

Reading a theorem statement and asking "is this really the thing I care about?" is the skill that matters. A proof of the wrong claim is worth nothing.

Now try the same claim on the buggy rule. This is what Lean says:

theorem buggy_pages : pages stepBuggy 0 (List.replicate 3 .conflict) = true := by
  decide

error: Tactic `decide` proved that the proposition
  pages stepBuggy 0 (List.replicate 3 Cause.conflict) = true
is false

That's the useful way to fail. Lean doesn't just say no. It hands back the exact input that breaks your claim. I now write the claim and try it on the buggy version first, so I know the claim can fail before I trust it passing.

Does the proof describe your real code?

Here's the catch from earlier. Everything above is about the Lean model. Your TypeScript is a separate program, and nothing so far says they behave the same.

The fix is a differential test: run the same inputs through the model and through the real code, and compare the answers. Because the model is also a program, Lean can print its answers. Add this to the end of Retry.lean:

/-- Every list of causes up to length `n`. -/
def allRuns : Nat → List (List Cause)
  | 0     => [[]]
  | n + 1 => [] :: ([Cause.conflict, Cause.other].flatMap fun c => (allRuns n).map (c :: ·))

def code : Cause → Char
  | .conflict => 'c'
  | .other    => 'o'

/-- One line per run: the run as letters, then the model's answer. -/
def main : IO Unit := do
  for run in allRuns 8 do
    let name := String.ofList (run.map code)
    IO.println s!"{name} {pages stepFixed 0 run}"

lean --run Retry.lean now prints an answer for every run of up to 8 failures. That's 511 runs: 1 empty run plus 2 + 4 + … + 256. The test below reads that output and runs the same inputs through the real function. Here the "real code" is a TypeScript version of the rule, with a flag to switch the old bug back on.

const LIMIT = 3;
type Cause = "conflict" | "other";

// The real code under test. `reset` turns the old bug back on.
function pages(causes: Cause[], reset: boolean): boolean {
  let streak = 0;
  for (const cause of causes) {
    streak = reset && cause === "conflict" && streak + 1 >= LIMIT ? 0 : streak + 1;
    if (streak >= LIMIT) return true;
  }
  return false;
}

// Lean prints one line per run: "<c|o letters> <true|false>".
const lines = (await Bun.$`lean --run Retry.lean`.text()).split("\n");
const cases = lines.map((l) => /^([co]*) (true|false)$/.exec(l)).filter((m) => m !== null);

for (const [label, reset] of [["fixed code", false], ["code with the old bug", true]] as const) {
  let mismatches = 0;
  let first = "";
  for (const m of cases) {
    const causes = [...m![1]].map((ch): Cause => (ch === "c" ? "conflict" : "other"));
    if (pages(causes, reset) !== (m![2] === "true")) {
      mismatches++;
      first ||= m![1] || "(empty run)";
    }
  }
  console.log(`${label}: ${cases.length} cases, ${mismatches} mismatches${first ? `, first: ${first}` : ""}`);
}

Run it with bun diff.ts. Here is what it printed for me:

fixed code: 511 cases, 0 mismatches
code with the old bug: 511 cases, 140 mismatches, first: ccc

That second line is the safety net. If someone reintroduces the bug, or changes the real code without updating the model, this test fails and tells you the shortest input that shows it. Checking every short run works well because bugs in state machines and counters nearly always show up on short inputs.

In my real projects the same pattern runs on thousands of cases: 1,847 on the job runner's retry logic, 2,225 on the music engine, 14,512 on the colour checker. All of them had zero mismatches after the fixes.

What's worth proving

I use one test for whether something is a candidate. Can I say it as "for every X, Y"? If I can, it's a candidate. If I can only say "it looks right", it isn't.

Things that fit well:

Retry, backoff and escalation rules. "However many times it fails, a human is told" is exactly this shape.
State machines with an invariant. "No key is ever left pressed", "never two workers on one task."
Time and ordering arithmetic. Tempo maths, scheduling, insert positions in a sorted list.
Validation and permission rules. "A token is accepted only if it was issued and has not expired."
Exact arithmetic where rounding hides problems, such as contrast ratios.

Things that don't:

User interfaces. A button's colour is a thing to look at.
Glue code that mostly calls other systems. There's no clean model to prove.
Anything you can't state in one sentence yet. Write the sentence first. Often that alone finds the problem.

My rule is to prove the small, hard, high-stakes cores and leave the rest to tests.

What it found in my first three days

The retry loop above is the first real find. It was in the job runner exactly as described, and I fixed it. Three more:

A timing bug in a music app. I have a shared jam tool where people play together. When the swing setting changed, the engine took its lead time from the pending swing instead of the committed one. In the case Lean found, at 200 bpm, notes were committed 37.5 ms early, and it failed at every tempo over 150. A second bug was in loop handling: after shortening a loop from four bars to three, it looped at bars 6 and 9 instead of 7 and 10.
Colours that failed their own claims. My site starter claims that 31 colour pairs pass accessibility contrast. Lean checked the exact ratios, with no rounding, and proved those 31. It also proved three other pairs fail. Two were decorative borders, at 1.30 and 1.74 to 1. The third was the dark-mode chart colour at 2.64 to 1, under the 3 to 1 a chart needs. I changed that colour and it's now 3.77.
A melody with a law. I'm making an album, and one track is built from a four-note motif that repeats inside itself, three levels deep. I wrote the rule that the pattern is self-similar and proved it. The checker then caught a real problem: one note was too high for the sampled instrument that plays it, and the export tool silently moved it down an octave, which broke the pattern in 76 of 1,248 places. I changed the motif so the note fits.

None of these were hard to understand once they were shown to me. None of them were found by a test I already had.

Where it hurts

The model can drift from the code. This is the big one. The differential test is what keeps it honest, and it only covers the inputs you generate. Treat the model as something that needs maintaining, like any other test.

Proofs rest on assumptions, and you should list them. Each of my proof projects has a short "modelled versus assumed" section. If I leave out how time works, or assume a function behaves, the proof is about that assumption. Write the list down. It's the part a reader most needs.

A claim can be true and useless. If the assumptions contradict each other, anything is provable. That's why I try the claim on the buggy version first. If it can't fail, it isn't telling me anything.

It's slow in one specific way. Importing a large library makes compiles heavy, as in the lake exe note above. The core-only files here are instant.

The learning curve is real. I can read a theorem and judge it. I can't yet write a proof like the one above from scratch, and I rely on an agent for that. If you want to write them yourself, the free book Theorem Proving in Lean 4 is the place to start.

Where I'd start on Monday

Find one function in your code with a comment that says "always" or "never."
Write it as a small pure model in Lean, as in Retry.lean. Data in, data out.
Write the comment as a claim and try it on the version of the code you suspect. Let it fail first.
Fix the model, prove the claim, then run the differential test against the real code.

The two free references I'd read are Functional Programming in Lean, which teaches the language for programmers, and Theorem Proving in Lean 4, which teaches the proofs. The main site is lean-lang.org.

If you try it, the thing to watch for is the moment a claim you were sure about gets a counterexample. That moment is the whole point. I'll write a follow-up when I've done this for longer than three days.

Lean for People Who Already Write Tests