Lean 4 online 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.
Run Lean 4 online
This playground is an online Lean 4 compiler: type a program or a proof, press Run, and Lean checks it. Start from an example in the menu, or open a code sample from the language guide. For guided practice, the Academy has interactive courses and the problem set has programming and proof challenges judged by Lean.
Is the Lean 4 playground free?
Yes. You get 10 runs without an account, and a free account gives 40 runs a month. The Academy Pass makes them unlimited.
Do I need to install Lean?
No. Your code is compiled by Lean 4 on our server and the results come back to the browser. When you are ready to work locally, the setup guide installs Lean with elan and VS Code.
Which Lean version runs, and is Mathlib available?
Lean 4.30 with its core library: Nat, Int, List, Array, String, IO and tactics such as simp, omega, decide and induction. Mathlib is not installed.
Can I prove theorems as well as run programs?
Yes. Write a theorem and its tactic proof; the Goals panel shows what is left to prove, like the infoview in VS Code. The tactics guide explains each tactic, and the problems give you proofs to write.
How do I share Lean code?
Press Share. The code travels inside the link itself and never reaches our server, so anyone who opens the link sees your file in their own playground.