# The Lambda Lab cookbook

```{admonition} What this part is
:class: tip
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](https://bnaskrecki.faculty.wmi.amu.edu.pl/lab-lambda/) 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](https://bnaskrecki.faculty.wmi.amu.edu.pl/lab-lambda/)
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](../appendix/cheatsheet.md) 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.