Little Leaner

A small pond: algae, snails and flies, frogs and fish, a duck, a heron and an otter. Eleven short lines say who eats whom. Ask a program whether the heron is above the algae and it may say yes. This book asks for more: a reason you can hold, check, and pass to another program. In Lean 4, the claim "the heron is above the algae" is a type, and a proof of it is a thing of that type. Lean checks the proof the way it checks any program, before anything runs and without trusting anyone.

That idea has a second half, and it is the one in the title. In Lean, a type can mention a value. A list can carry its length in its type, so asking for the first element of an empty list is not a crash at run time but a mistake Lean refuses to accept. Types like that are called dependent types. With them, a program can say what it promises, and a proof can show that it keeps the promise.

This little book teaches both ideas from zero, in the question-and-answer style of The Little Schemer. Each page has two columns, a short question on the left and a short answer on the right. Cover the answers with a card, try, then look. The question you will answer most often is "What is the goal now?", because proofs are written with Lean's tactics from the very first one, and the goal is the best teacher a beginner has. Now and then a box states a Maxim, a short rule the questions above it have earned, from "Every thing has a type. Ask #check before you guess." to "Make wrong programs impossible to write. Then prove the rest."

What you will learn

1. Things and Their Types. Critters, functions by cases, and what Lean refuses before anything runs.
2. Propositions Are Types. Claims as types, proofs as things, and the first tactics; then a look at the program a tactic built.
3. Rules as Constructors. "Above" as a rule that asks for evidence; goals that split in two; "if", "and", "or".
4. Nothing and Something. False and "not", "for every" and "there is": nothing eats the heron, and here is why.
5. Numbers by Hand. Numbers from two pieces, proofs by computing, and induction.
6. Equality. One constructor, what rfl can see, and rewriting when computing is not enough.
7. Lists and Their Laws. Append, length and reverse written by hand, and their laws proved for every list.
8. Types That Depend on Values. Vectors that know their length, a head with no empty case, and positions that cannot be out of range.
9. Families of Evidence. Even numbers, decisions that bring their evidence along, and critters that carry proof they can swim.
10. A Language That Cannot Go Wrong. Typed expressions, an evaluator that never fails, a stack machine whose stack cannot run dry, and a compiler proved to keep the meaning of every program.

Who it is for

Students and programmers who have never taken a logic course and never written a proof. You need some programming in any language, a pencil, and patience. No mathematics, no Mathlib and no prior Lean are assumed. You do not need to know what ∀ or Π means; by Chapter 8 you will have written both. The Little Elpier, the book this one follows, helps but is not required. A chapter is an evening's work.

What you get

• 10 short chapters, 752 questions with their answers, and 12 Maxims collected on one page
• 39 exercises graded ★ to ★★★, each with a solution that Lean checks
• 12 diagrams: the food web, proof trees, goals that split, induction, a vector's length in its type, compile-then-run
• A reference card of every command and tactic, with how to read it aloud, and a guided "Where to Go Next"
• The Apache-2.0 companion code at github.com/Volland/little-leaner: every program in the book, with every printed output, error and goal kept as a golden file that a test checks

Every example is checked

Everything runs on core Lean 4 (version 4.35.0), with no libraries to install beyond Lean itself. One lake build sets up the pond on macOS, Linux and Windows. Open the companion code in VS Code with the Lean 4 extension and every goal in the book appears beside the proof as you move through it.