Lean Grimoire

Select one or more potions on your bench; the recipes light up with the statements they let you brew from that selection. Click a brew to add it to your bench — and watch the corresponding have appear in the spellbook. Craft the goal to finish the proof (the sorry turns into the final step). Undo steps back; names like hAB are auto-chosen but the objects and their types are kept typographically distinct. The Lean produced is deliberately plain, step-by-step pseudo-Lean — the point is to see the proof being built, not to write the slickest tactic.

The ★ tutorial levels — 1.1, 2.1, and so on up to 20.1 — each introduce one new mechanic, and each carries a hint under the goal naming the first move to make. The practice levels in between carry none: by then the mechanic is yours.

This is not a full Lean tutorial, and it teaches only a small subset of the available Lean tactics. In particular, the powerful ability of Lean tactics to modify the goal is completely untapped here: every move works forwards, from what you already have towards the goal, whereas real Lean proofs freely work backwards as well. The automation that does most of the work in practice — simp, omega, decide, exact?, and the rest — is absent by design, since the point of the game is to perform each logical step yourself.

For the same reason, the Lean written out as you play should not be taken as an indication of best practice for idiomatic Lean code. It is deliberately plain and step-by-step so that the shape of the proof stays visible; an experienced Lean user would write most of these proofs in a line or two. To learn Lean properly, start with the Lean community's learning resources.

Each chapter here is one mechanic: chapter N opens with exercise N.1, the level that introduces the mechanic, and the rest of the chapter is practice that needs nothing newer. So the twenty tutorial levels are exactly 1.1, 2.1, …, 20.1, and an exercise never depends on a higher number than its own.

That numbering is Grimoire's own, and it does not follow QED, whose sections are organised by topic instead. Where a level descends from a QED exercise it says so under the goal — and says when QED states the same thing differently, which is usually QED's assumption environments where Grimoire uses an implication, or its group-theory sections, which carry the axioms as hypotheses where Grimoire puts them in the theory of the sort. QED's own sections on free variables and on "push"/"pull" have no counterpart here: Grimoire makes no distinction between free and bound variables, so those moves have nothing left to do. Some chapters are new, and about a fifth of the levels have no QED ancestor at all.