Lean docs

Examples

Saved locally
λWelcome.lean
Lean runs on your device

First use downloads the Lean compiler (~46 MB). It runs as WebAssembly in your browser; your code is not uploaded. The download is cached for later runs.

No output yet

Run your program to see its output here. ⌘ ↵

First use downloads the Lean compiler (~46 MB). It runs as WebAssembly on your device; your code is not uploaded. The download is cached.

Settings

Appearance

Editor layout

Lesson progress

0 of 17 lessons completed on this device.

Keyboard shortcuts

Run current file⌘ / Ctrl + Enter
Search the current section⌘ / Ctrl + K
Save workspaceAutomatic
Insert a Unicode symbol\to + Enter

Support leanlab

Donate Zcash to support the project.

About this workspace

The first use downloads the Lean compiler and core library (~46 MB), then caches them. Lean 4.33.0-pre runs as WebAssembly on your device; your code is not uploaded. Files are independent; Mathlib and custom imports aren’t bundled. A desktop browser is recommended.

Powered by the community’s Lean WASM runtime