Lean playground
Write definitions, evaluate expressions and work through proofs. Keep several scratch files, share any of them with a link.
10 free runs without an account · sign up for 40 a month
\to in the editor, or click:Results of #eval and #check appear here.
Run with ▶ Run or Ctrl + Enter. Type \to, \forall or \and for →, ∀ and ∧.
What runs here
Lean 4.30 with its core library: Nat, Int, List, Array, String, IO, and the standard tactics such as simp, omega, decide and induction. Each run has a 15-second limit. Mathlib is not installed.
Reading results
Output shows #eval and #check results. Problems lists every error and warning with a line to jump to. Goals shows unsolved goals with their hypotheses, like the infoview in VS Code.
Your files
Files are saved in this browser, separately for each account. Double-click a file name to rename it, download it as .lean, or share it: the code travels in the link itself and never reaches our server. A file containing sorry compiles with a warning, which marks an unfinished proof.