Lab🔗

Coming soon.

The Lab lets you write any Lean, see the goal at each line, and Audit a file with the five-step checklist. Running new code needs a Lean server, which this site does not have yet. Everything else works here: the lessons, Practice and the Advanced cases. The Lean shown with each example was checked by Lean when the site was built, and hovering over it shows what Lean knows.

Meanwhile, to experiment with Lean in your browser, the official editor at live.lean-lang.org runs Lean and Mathlib (without the audit). Or run this site on your own computer, Lab included: see the README.