← All repos

mathlib4

The math library of Lean 4

GitHubleanprover-community.github.io/mathlib4_docs
lean4
Browse cluster: Lean4 Formal Verification & Cryptography →
33,719commits
787contributors
7languages

Tech stack & purpose

Mathlib4 is the mathematical library for the Lean 4 proof assistant. The project contains formalized mathematics spanning multiple domains, organized into several components: the main Mathlib library providing general-purpose mathematical definitions and theorems; an Archive section for formalization projects without a natural home in the core library, including solutions to International Mathematical Olympiad problems and theorems from Freek Wiedijk's 100 theorems list; a Cache system for downloading pre-built artifacts to accelerate compilation; and testing infrastructure. The project is built in Lean 4 and is maintained by the Lean community.

Community & reference links

Languages

Lean
99.6%
Python
0.3%
Shell
0.0%
TeX
0.0%
Dockerfile
0.0%
HTML
0.0%
ASL
0.0%

Contributors (top 30 of 787)