Little Leaner

A little book of dependent types

The Little Leaner

Dependent Types and Proofs in Lean 4, One Question at a Time

Volodymyr Pavlyshyn

This book keeps the reasons. It uses Lean 4, a programming language in which a claim such as "the frog eats flies" is a type, and a reason for the claim, a proof, is a thing of that type. Lean checks proofs the way it checks programs: before anything runs, and without trusting anyone. If Lean accepts a proof, the claim holds.

Buy on Leanpub Read a sample
The cover of The Little Leaner: an engraved scene of a young scholar and a small robot reading under a blossoming tree, among scrolls of logic and a ∀ sign.

A small book about a big idea: a type can say what a program promises, and a proof is a program that keeps the promise.

The Little Leaner teaches dependent types and proofs in Lean 4, one question and one answer at a time, in the style of The Little Schemer. Cover the right-hand column, read the question, answer it, then look.

Start with a pond and the types of its critters. Prove who eats whom. Climb through and, or, not, for every and there is; numbers, equality and induction; lists, and vectors whose types know their length. Finish with a little language whose programs cannot go wrong, and a compiler to a stack machine that is proved to keep their meaning.

The sequel to The Little Elpier, which is not required.

10 chapters, 760 questions, 12 Maxims, and graded exercises at the end of every chapter, each with a solution that Lean checks.

From a pond to a proved compiler

The book starts with eight critters in a pond and a table of who eats whom. It ends with a little programming language whose bad programs cannot be written, and a compiler for it that Lean has checked keeps the meaning of every program. Each step uses the one before:

No logic course and no mathematics are assumed, only some programming. Every program, output and proof goal printed in the book is checked by Lean 4, so the book cannot quietly drift from what Lean says.

Get the book

The Little Leaner is on Leanpub as a PDF and an EPUB. Buy it once, and every future update is yours too. A book like this takes months to write; buying it pays for the work, and for the next book.

Leanpub

PDF and EPUB, with every future update free. Leanpub also has a free sample.

Buy on Leanpub

Try it first

Read two sections of Chapter 2 below, and run every program in the book from the free companion code.

Read the sample Get the code

Cite it as
Pavlyshyn, V. (2026). The Little Leaner: Dependent Types and Proofs in Lean 4, One Question at a Time. https://volland.github.io/little-leaner/

Read it the way the book reads

Each page is two columns: a question on the left, its answer on the right. Cover the answers, try each question, then look. Here are two sections of Chapter 2, where the first proofs appear.

The First Theorem

How do we tell Lean that the frog eats flies, and keep the proof?

We write a theorem:

theorem frog_eats_fly : Eats frog fly := by
  exact Eats.frog_fly

Lean accepts it and prints nothing.

How do we read it?

theorem gives the proof a name, frog_eats_fly. After the colon comes the claim. After := comes the proof.

And by?

by starts a list of tactics. A tactic is a small step that builds part of a proof for us. This proof has one step.

What is the goal before the first tactic?

⊢ Eats frog fly

A goal is what is still missing. Read ⊢ as "show that". We must show that the frog eats flies.

Where does that goal come from?

From the claim after the colon. Before any tactic runs, the whole claim is missing.

What does exact Eats.frog_fly do?

It hands Lean a thing and says "this has exactly the type of the goal". Lean checks that it does. Eats.frog_fly has type Eats frog fly, which is the goal.

What is the goal now?

There is none. The proof is complete, and Lean says nothing.

How can we be sure nothing is left?

Ask for one more step:

example : Eats frog fly := by
  exact Eats.frog_fly
  exact Eats.frog_fly
error: No goals to be solved

The second exact has nothing to do.

What is example?

A theorem with no name. Lean checks it and then forgets it. We use example when we only want to see that something checks.

Could we have named the theorem something else?

Yes. The name is ours to choose. Lean checks only the claim and the proof.

What happens if we hand exact a critter?

example : Eats frog fly := by
  exact frog
error: Type mismatch
  frog
has type
  Critter
of sort `Type` but is expected to have type
  Eats frog fly
of sort `Prop`

frog is a thing, but a thing of the wrong type. It is a critter, not a proof that the frog eats flies.

What is a sort?

Lean's word for the type of a type. Critter lives in Type, the sort of data. Eats frog fly lives in Prop, the sort of claims.

What is the type of frog_eats_fly?

frog_eats_fly : Eats frog fly

The same as the type of Eats.frog_fly. A theorem is a name for a proof.

Can we use that name in another proof?

Yes, anywhere a proof of Eats frog fly is wanted:

example : Eats frog fly := by
  exact frog_eats_fly

Must we always write Eats. before the constructor?

No. Lean knows the goal is an Eats claim, so a leading dot looks the name up inside Eats:

example : Eats heron fish := by
  exact .heron_fish

What if we do not remember the name of the constructor at all?

Let Lean find it:

theorem heron_eats_fish :
    Eats heron fish := by
  constructor

What is the goal before constructor?

⊢ Eats heron fish

What does constructor do with it?

It tries the constructors of Eats, one by one, until it finds one whose type matches the goal. Here that is heron_fish. The goal is then met, so no goals are left.

Two proofs, one per row: each starts from a goal, one tactic supplies a thing of that type, and no goals are left.
Two proofs, one per row: each starts from a goal, one tactic supplies a thing of that type, and no goals are left.

A Claim With No Proof

Can constructor prove Eats fly frog?

example : Eats fly frog := by
  constructor
error: Tactic `constructor` failed: no
  applicable constructor found

⊢ Eats fly frog

No. Lean also shows the goal it could not meet.

Why did it fail?

None of the eleven constructors has the type Eats fly frog. The closest one, frog_fly, has the critters the other way round.

What if we hand Lean that one anyway?

error: Type mismatch
  Eats.frog_fly
has type
  Eats frog fly
but is expected to have type
  Eats fly frog

The same kind of error as "frog" in place of a critter. A proof of the wrong claim is a thing of the wrong type.

So is Eats fly frog false?

We believe so. But Lean has not said so. A tactic failed, and that is all.

What is the difference?

"Not proved" means no one has found a proof. "False" would need a proof that no proof can exist. Chapter 4 learns to write that.

Did Chapter 1's decide not say "is false"?

It did, about eats fly frog = true. decide could compute the Boolean false and see it is not true. With Eats there is no Boolean to compute, only constructors to look for.

Contents

Preface · Before You Begin

  1. 1

    Things and Their Types

    The pond is back. Algae grow in it. Snails and flies eat the algae. Frogs and fish eat the snails and the flies, a duck eats whatever it can reach, and a heron and an otter stand at the top and eat the frogs and the fish.

    59 questions · the First Maxim

  2. 2

    Propositions Are Types

    At the end of Chapter 1, Lean agreed that eats frog fly is true. It worked the answer out from a table we wrote. If we had made a mistake in the table, it would have agreed with the mistake as calmly.

    65 questions · the Second Maxim and the Third Maxim

  3. 3

    Rules as Constructors

    Is the heron above the algae? Look at the food web and you will say yes at once. The heron eats the frog, the frog eats the fly, and the fly eats the algae. But Lean knows only Eats, and no constructor of Eats says Eats heron algae. In Chapter 2, a claim with no constructor behind it could not be proved.

    77 questions · the Fourth Maxim and the Fifth Maxim

  4. 4

    Nothing and Something

    In Chapter 2 we tried to prove that the fly eats the frog. No constructor of Eats fit, and Lean refused every attempt. But a claim we cannot prove is not yet a claim we have shown to be false. Maybe we did not try hard enough.

    79 questions · the Sixth Maxim and the Seventh Maxim

  5. 5

    Numbers by Hand

    The heron stands at the top of the pond. Chapter 3 proved that it is above the algae. It did not say how far above. How many steps is it from the heron down to the algae?

    75 questions · the Eighth Maxim

  6. 6

    Equality

    Every chapter so far has used =. Chapter 1 checked that eats frog fly = true, and Chapter 5 proved 0 + n = n by induction. We never asked what = itself is, or where its proofs come from.

    70 questions · the Ninth Maxim

  7. 7

    Lists and Their Laws

    The heron eats a frog, the frog eats a fly, and the fly eats algae. Write them in a row and you have a food chain: [heron, frog, fly, algae]. A row of critters is a list.

    79 questions

  8. 8

    Types That Depend on Values

    Ask a list of critters for its first critter, and most of the time there is one. But a list can be empty. Ask with head?, and Lean's lists answer with a shrug that every caller must check, even a caller who knows the list is not empty.

    84 questions · the Tenth Maxim

  9. 9

    Families of Evidence

    In Chapter 1, by decide checked that eats frog fly = true. Lean computed the Boolean, found true, and agreed. In Chapter 2 we traded the Boolean for something better: a type, Eats frog fly, whose things are proofs.

    84 questions · the Eleventh Maxim

  10. 10

    A Language That Cannot Go Wrong

    The Little Elpier ended with a type checker. It read a small expression such as add tt (num 1), which asks us to add true to the number one, and said Failure. The bad expression was written first and turned away after. A type checker is a guard at the door.

    88 questions · the Twelfth Maxim

The Maxims · The Little Leaner's Card · Solutions · Where to Go Next

The twelve Maxims

Short rules, each earned by the questions of one chapter.

  1. The First Maxim

    Every thing has a type. Ask #check before you guess.

    Chapter 1
  2. The Second Maxim

    A proposition is a type. A proof is a thing of that type.

    Chapter 2
  3. The Third Maxim

    A tactic builds a proof. The goal says what is still missing.

    Chapter 2
  4. The Fourth Maxim

    A rule is a constructor. To use it, apply it and prove what it asks for.

    Chapter 3
  5. The Fifth Maxim

    To prove "and", prove both. To use "or", handle both.

    Chapter 3
  6. The Sixth Maxim

    To prove "not P", assume P and reach False. From False, anything follows.

    Chapter 4
  7. The Seventh Maxim

    To prove "for every", take any one. To prove "there is", show one.

    Chapter 4
  8. The Eighth Maxim

    A proof about a recursive function follows the function: induction where it recurses.

    Chapter 5
  9. The Ninth Maxim

    Equal means the same after computing. When computing is not enough, rewrite.

    Chapter 6
  10. The Tenth Maxim

    A type may mention a value. Then checking the type checks the value.

    Chapter 8
  11. The Eleventh Maxim

    Evidence is data. What you can decide, let Lean decide.

    Chapter 9
  12. The Twelfth Maxim

    Make wrong programs impossible to write. Then prove the rest.

    Chapter 10

Get the code

Every program in the book comes from the companion repository, and every output, error and goal printed in the book is a golden file there that a test checks. It needs only core Lean 4.35.0: no Mathlib and nothing else to download. It runs on macOS, Linux and Windows.

On your machine

Install elan, the Lean installer. The first build fetches the right Lean.

git clone https://github.com/Volland/little-leaner
cd little-leaner
lake build
lake env lean ch01/hello.lean
python3 tests/run_lean.py

In an editor

Open the folder in Visual Studio Code with the Lean 4 extension. The infoview shows the goal at the cursor, the same goals the book prints.

In the browser

No install: paste lib/Pond.lean and a chapter file into the Lean web editor. It runs the newest Lean, so a message may read a little differently.