Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place.

Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Lean mathematical theories

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 mathematicians might be interested in.

Note that there are many other things within these libraries which are not documented here (for example red black trees and so on); these missing definitions and theorems may well be of interest to computer scientists.

• Functions between types

• Relations on types, quotients

• Partial and total orders, lattices

• Sets and set like objects

• Categories

• The natural numbers

• The integers

• Groups

• Rings and fields

• Linear algebra

• Number theory

• Topological, uniform and metric spaces

• Measure theory