Playground
A Lean 4 scratchpad in your browser.
Write a Lean 4 program or proof. Run it in an isolated sandbox with Lean’s core library, then read the result, errors and open goals below.
Loading editor…
Type
\to, \and, \< … to insert symbols while typingResults of #eval and #check appear here. Press ▶ Run or Ctrl/⌘ + Enter.
ReadyLn 1, Col 1UTF-8Lean 4
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. 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.
A word on sorry
A file containing sorry compiles with a warning. That is an unfinished proof, not a verified result, and it never counts as a completed exercise.