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, std4, and mathlib4.
Binary
There are binary packages available for all major platforms here:
Nightly builds are available here:
Source
The source code can be downloaded here:
Editor Support
There are Visual Studio Code and Emacs extensions, each of which support interactive editing.
-
Visual Studio Code is available for all major platforms. The Lean 4 extension is available in its marketplace.
-
Emacs: lean4-mode is a major mode for Emacs 27.1 or newer.
Lean 3
Below are the official releases of Lean 3. For the extended community version of Lean 3, please see the community website.
Binary
There are binary packages available for all major platforms here:
All previous releases are available here:
Source
The source code can be downloaded here: