Lean and its Mathematical Library #
The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura.
The Lean mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. The library also contains definitions useful for programming. This project is very active, with many regular contributors and daily activity.
You can get a bird's-eye view of what is in the mathlib library by reading the library overview, and read about recent additions on our blog. The design and community organization of mathlib are described in the 2020 article The Lean mathematical library, although the library has grown by more than an order of magnitude since that article appeared. There is also a paper (arXiv version) about the challenges with mathlib's growth, on a technical and social level.
You can also have a look at our repository statistics to see how the library grows and who contributes to it.
Try it!
You can try Lean in your web browser, install it in an isolated folder, or go for the full install. Lean is free, open source software. It works on Linux, Windows, and MacOS.
Learn to Lean!
You can learn by playing a game, following tutorials, or reading books.
- Learning resources
- Theorem Proving in Lean 4 (an introduction)
- API documentation of mathlib
Meet the community!
Lean has a very diverse and active community. It gathers mostly on a Zulip chat and on GitHub. You can get involved and join the fun!
What is a proof assistant? #
A proof assistant is a piece of software that provides a language for defining objects, specifying properties of these objects, and proving that these specifications hold. The system checks that these proofs are correct down to their logical foundation.
These tools are often used to verify the correctness of programs. But they can also be used for abstract mathematics, which is something of interest to the mathlib community. In a formalization, all definitions are precisely specified, and all proofs are virtually guaranteed to be correct.
For what has been formalized with Lean and mathlib, see the list of papers and the list of projects.