The Lambda Lab cookbook

What this part is

The six lectures build the theory in order. This part is the playground: long satisfying calculations, a graded puzzle collection with hidden solutions, the folklore and curiosities that make the λ-calculus unforgettable, and a guided parade of everything the Lambda Lab can do.

Every output printed here was produced by the actual engine — nothing is typeset by hand. When a computation hits the lab’s honesty limits, we show that too: it is part of the mathematics.

How to read this part: don’t. Open the lab in a second tab, and run it. Single commands are clickable deep links; multi-step recipes are meant to be pasted line by line into one session (the terminal remembers your let definitions; defs lists them). If a command is unfamiliar, help <command> in the lab explains it with examples, and the cheatsheet has the whole map on one page.

The four chapters, in reading order:

1. Grand calculations — Fibonacci without recursion, factorial two ways, Ackermann in one line, Boolean circuits verified exhaustively, and the exponential cliff where honesty kicks in.

2. Puzzles and extended exercises — predict-then-check binding puzzles, encoding challenges, principal-type guessing games, and a prove ladder, all with dropdown solutions.

3. Curiosities and lore — the predecessor legend, the term that means both FALSE and 0, the Ω that grows, fixed points of everything, and the combinator zoo.

4. What this lab can do — the feature parade, from the highlighted traces to the full Curry–Howard round-trip into Live Lean.