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.
Editor Support
There are Visual Studio Code, Neovim, and Emacs extensions, each of which support interactive editing.