MiniLean4

# the polymorphic identity on propositions: for every P, P -> P.
goal forall (P : Sort 0), P -> P
intro P
intro p
exact p
qed

What this book is

Interactive theorem provers such as Lean, Coq, and Agda rest on a small core: a kernel that decides whether a term has a given type. Everything else, including tactics, notation, and automation, is scaffolding that produces terms for the kernel to check. If the kernel is right, a bug anywhere else can make the system fail to prove a theorem, but never make it accept a false one.

MiniLean4 is a proof assistant kernel at teaching scale: the same kind of dependent type theory that Lean 4, Coq, and Agda use for formal verification, cut down to what fits in a few files of Rust. If you want to understand how Lean 4 checks a proof, what the Curry-Howard correspondence buys you in practice, or where formal verification tools get their trust, this is the machinery with nothing hidden.

The goal here is to make that kernel concrete. Each chapter introduces one idea on paper, states it precisely, and then shows the Rust code that implements it. The whole implementation, kernel plus tactics and parser, is under three thousand lines with no dependencies, and this book covers all of it.

The book is self-contained. You need to be comfortable reading a recursive function and a little set notation. No prior exposure to type theory or to Lean is assumed, although readers who know Lean will recognize much of what they see.

How to read it

Part I builds a type checker for a dependent type theory and shows that it is a proof checker for a logic. Part II adds inductive types (natural numbers, trees, lists, vectors, and equality) and a tactic language that writes proof terms for you. Part III opens the black boxes that Parts I and II relied on: substitution, alpha-equivalence, and reduction, where kernel bugs hide. Part IV explains why universes are structured as they are, and states the metatheory. The appendices contain the full proofs, the paradox that justifies the universe design, and a reference for the script language.

Throughout the book you will meet four kinds of interactive element.

• Playgrounds run the kernel. Edit the script, press run, and read the transcript.
• Explorers show the kernel's own view of a term: its syntax tree, its typing derivation rule by rule, its reduction one step at a time, which binder each variable belongs to, and the proof state after every tactic. Every explorer is live: change the term and the kernel recomputes.
• Steppers walk through an algorithm one step at a time, showing the state after each step.
• Trace trees show the exact sequence of recursive calls the type checker makes on a term, with the typing rule each call corresponds to.

Callouts marked in the code point to the Rust function that implements what was just defined. Exercises come with solutions, folded away until you want them.

Running the code yourself

The repository contains the kernel, a command-line runner, and the example scripts used in this book.

cargo run -- examples/identity.leanmini
cargo run -- examples/nat-reflexivity.leanmini
cargo run -- examples/zero-add.leanmini
cargo run -- examples/generic-list.leanmini
cargo run -- examples/generic-vec.leanmini
cargo test

Running cargo run with no arguments starts an interactive session that accepts the same commands one line at a time. Appendix E describes the language.

The source is organized to follow the book.