Make an idea executable.

Write a small Lean program or proof and check it here. The compiler includes Lean’s bundled core libraries. This initial playground does not install external packages or include Mathlib.

Each run has a 15-second limit. Your draft stays in this browser; completed course exercises are saved to your account.

A file containing sorry can compile with a warning. That is an unfinished proof, not a verified result.