What does Lean already know?

UPDATE Dec 2019: the page below is historical. I wrote it when I was learning Lean and Lean knew barely any undergraduate level mathematics. A much better answer to what Lean knows now is here , or you can just click on the “What maths is in Lean?” link above.

Here is the original post from Jan 2018.


The core Lean library (imported automatically) and mathlib, the mathematics library, between them know quite a lot of basic undergraduate-level mathematical definitions. This page is an overview of the definitions and lemmas within these libraries that I think mathematicians might be interested in.

Note that there are many other things within these libraries which I have not documented here (for example red black trees and so on);  these missing definitions and theorems may well be of interest to computer scientists. What is here is, of course, to a certain extent a reflection of my personal tastes.

Note that this page will necessarily age with time; the last time it was updated was 23rd Jan 2018. All the Lean code here should run with any version of Lean compiled on or after this date.


Rings and fields

Partial and total orders

Functions between types

Relations on types

Quotients and equivalence classes


The natural numbers

The integers.

To do: init/data/fin (certain finite sets) and all of mathlib (other than nat and int) [note that I have done most of mathlib “in rough”, it’s just a case of finding the time to type it up here.]