Download

Lean 4

Stable releases of Lean 4 are published approximately once per month, after a series of release candidates for community testing.

Please follow the official instructions unless you know that you need to directly download one of these releases.

There is also an online version providing recent versions of Lean 4, batteries, and mathlib4.

Quickstart | Source Code

Editor Support

There are Visual Studio Code, Neovim, and Emacs extensions, each of which support interactive editing.