Lean and its Mathematical Library #

The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura.

The community is currently in the middle of switching from using Lean 3 to using Lean 4. This website is still being updated, and some pages have outdated information about Lean 3 (these pages are marked with a prominent banner). The old Lean 3 community website has been archived .

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 an order of magnitude since that article appeared. You can also have a look at our repository statistics to see how the library grows and who contributes to it.

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.

Try the online version of Lean

Installation instructions

Working on Lean projects

Lean has very diverse and active community. It gathers mostly on a Zulip chat and on GitHub . You can get involved and join the fun!

Meet us

How to contribute

Papers involving Lean

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.

Formalized with Lean and mathlib

The cap-set problem

by Dahmen, Hölzl and Lewis

In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of $𝔽^n_q$ with no three-term arithmetic progression. This problem has received much mathematical attention, particularly in the case $q = 3$, where it is commonly known as the cap set problem. Ellenberg and Gijswijt's proof was published in the Annals of Mathematics and is noteworthy for its clever use of elementary methods. Learn more

Perfectoid spaces

by Buzzard, Commelin and Massot

Perfectoid spaces are sophisticated objects in arithmetic geometry introduced by Peter Scholze in 2012. We formalised enough definitions and theorems in topology, algebra and geometry to define perfectoid spaces in the Lean theorem prover. This experiment confirms that a proof assistant can handle complexity in that direction, which is rather different from formalising a long proof about simple objects. Learn more

Independence of the continuum hypothesis

by Han and van Doorn

The continuum hypothesis states that there is no cardinality between the smallest infinite cardinal and the cardinality of the continuum. It was posed by Cantor in 1878 and was the first problem on Hilbert’s list of twenty- three unsolved problems in mathematics. Gödel and Cohen proved this is independent, i.e. neither provable nor disprovable, from ZFC. Learn more

Data Types as Quotients of Polynomial Functors

by Avigad, Carneiro and Hudon

A broad class of data types, including arbitrary nestings of inductive types, coinductive types, and quotients, can be represented as quotients of polynomial functors. This provides perspicuous ways of constructing them and reasoning about them in an interactive theorem prover. Learn more