- What is Lean?
Lean is a new open source theorem prover being developed at Microsoft Research. It is a research project that aims to bridge the gap between interactive and automated theorem proving. Lean can be also used as a programming language. Actually, some Lean features are implemented in Lean itself.
- Are pull requests welcome?
In the past, we accepted most pull requests. This practice produced hard to maintain code, performance problems, and bugs. It takes time to review a pull request and make sure it is correct, useful and is not in conflict with our plans. Small bug fixes (few lines of code) are always welcome. Any other kind of unrequested pull request is not. Thus, before implementing a feature or modifying the system, please ask whether the change is welcome or not.
- Should I use Lean?
Lean is under heavy development, and we are constantly trying new ideas and tweaking the system. It is a research project and not a product. Things change rapidly, and we constantly break backward compatibility. Lean comes "as is", you should not expect we will fix bugs and/or add new features for your project. We have our own priorities, and will not change them to accommodate your needs. Even if you implement a new feature or fix a bug, we may not want to merge it because it may conflict with our plans for Lean, it may not be performant, we may not want to maintain it, we may be busy, etc. If you really need this new feature or bug fix, we suggest you create your own fork and maintain it yourself.
- Where is the documentation?
The Lean tutorial is a good introduction to the system. It may contain a few inconsistencies due to recent changes, but we try to keep it in sync. The reference manual is work in progress, and we don't know when it will be ready. The core and math libraries contain many definitions and proofs, they demonstrate how we expect the system to be used. If the lack of documentation is an issue, then Lean is not a good match for you. Documentation is not the main priority right now. Recall that Lean is a research project and not a product. A public and very active chat room dedicated to Lean is open on Zulip. It is a good place to interact with other Lean users. You may also join the Lean user forum on Google Groups.
- Should I use Lean to teach a course?
Lean has been used to teach courses on logic, type theory and programming languages at CMU and the University of Washington. The lecture notes for the CMU course Logic and Proof are available online. If you decide to teach a course using Lean, we suggest you prepare all material before the beginning of the course, and make sure that Lean attends all your needs. You should not expect we will fix bugs and/or add features needed for your course.
- Are there IDEs for Lean?
Yes, the two main ones are for Emacs and VS Code. The Emacs Lean mode is available via MELPA. The VS Code Lean extension is available on its marketplace.
- Is Lean sound? How big is the kernel? Should I trust it?
Lean has a relatively small kernel. The leanchecker is a bare-bones version of the Lean kernel.
There are also two independent checkers: tc and trepplein.
We have implemented several kernel extensions to improve performance and make sure the system is reasonably responsive for interactive use.
We strongly recommend you frequently check your project without these extensions. The command line option -t0 disables all of them.
As far as we know, no proof of false has ever been accepted by Lean when using -t0.
If you are really concerned about soundness, we recommend you often export your project and recheck it using the independent checkers above.
- Should I open a new issue?
We use github to track bugs and new features. Bug reports are always welcome, but nitpicking issues are not (e.g., the error message is confusing). RFC issues are created by developers only.