No installation needed — this is the official Lean 4 web playground, embedded below. Type Lean code on the left and see the goal state / #check/#eval output on the right, exactly like the book’s examples.

↗ Open in full playground (new tab)

---

New to Lean? Start with Chapter 0: Setting up Lean 4 for a local install, or just start typing in the playground above — it already has Lean 4 and (a subset of) Mathlib loaded, no toolchain needed.