Need help with lean?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

leanprover-community
177 Stars 44 Forks Apache License 2.0 14.1K Commits 99 Opened issues

Description

Lean Theorem Prover

Services available

!
?

Need anything else?

Contributors list

logo

License Continuous integration Chat
github actions Bors enabled Join the Zulip chat

About

Installation

If you want to use Lean, the recommended way to install Lean is following these instructions under Regular install.

If you want to modify the code of Lean or the core library, the recommended way is to build Lean from source.

If you want to modify a single file in the core library (not the C++ source), then instead of building Lean from scratch, you can run (in your local

lean/
directory)
git checkout v3.xx.x
git checkout -b my-branch-name
elan override set leanprover-community-lean-3.xx.x
You can now build the core library with
lean --make library
or open any Lean file is VSCode / Emacs and it will use the version of Lean you specified. You might have to restart Lean (in VScode:
ctrl+shift+P Lean: Restart
). Warning: all imported Lean files will be from the downloaded community version, not the version of the files in this repository. Therefore, this setup is not recommended if you modify more than one file. Moreover, editor features like
Go to Definition
will not behave correctly with this setup. For the best experience, build Lean from source.

Stable binary releases of Lean are available on the release page. Nightly binary releases are available on the nightly release page.

Miscellaneous

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.