Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt

Use this file to discover all available pages before exploring further.

Mathlib is the comprehensive mathematical library for the Lean 4 theorem prover, maintained by the leanprover-community. It contains formal proofs spanning virtually every area of modern mathematics — from elementary number theory and group theory through measure theory, algebraic geometry, and condensed mathematics. The library is organized as a hierarchy of modules all collected under a single Mathlib/ directory, with a root Mathlib.lean file (8,234 lines) that publicly imports every module, making it possible to access all of Mathlib with a single import Mathlib.

​
Module Hierarchy

Every Mathlib file lives at a path like Mathlib/<Domain>/<Subdomain>/<File>.lean and is accessed via the corresponding dotted module name, e.g. Mathlib.Algebra.Ring.Basic. Building a specific file is as straightforward as: 
lake build Mathlib.Algebra.Group.Defs
The root import file aggregates everything: 
-- Mathlib.lean (8234 lines)
import Mathlib.Algebra.AddConstMap.Basic
import Mathlib.Algebra.Algebra.Basic
-- ... 8000+ further imports

​
The 33 Top-Level Domains

Mathlib’s Mathlib/ directory contains 33 top-level subdirectories, each corresponding to a major branch of mathematics or infrastructure:

Algebra

Groups, rings, fields, modules, algebras, polynomial rings, and Galois theory. The largest single domain in Mathlib.

AlgebraicGeometry

Schemes, presheaved and sheaved spaces, morphisms, and the machinery of modern algebraic geometry.

AlgebraicTopology

Simplicial sets, chain complexes, and homological constructions bridging topology and algebra.

Analysis

Real and complex analysis, calculus, measure theory, functional analysis, and Fourier analysis.

CategoryTheory

Functors, natural transformations, adjunctions, limits, monoidal and abelian categories, and sheaves.

Combinatorics

Graph theory, Ramsey theory, additive combinatorics, set families, and enumerative results.

Computability

Turing machines, computable functions, the halting problem, Rice’s theorem, and Turing degrees.

Condensed

Condensed sets and condensed modules following Clausen–Scholze’s framework.

Control

Infrastructure for monad transformers and control-flow abstractions used in tactic code.

Data

Foundational data structures: lists, arrays, finsets, multisets, hash maps, and trees.

Deprecated

Legacy modules preserved for backwards compatibility; users should migrate to current replacements.

Dynamics

Circle dynamics, omega-limit sets, fixed and periodic points, and translation numbers.

FieldTheory

Algebraic and transcendental extensions, splitting fields, Galois correspondence, and Abel-Ruffini.

Geometry

Affine and Euclidean geometry, differentiable manifolds, Lie groups, and smooth vector bundles.

GroupTheory

Subgroups, quotient groups, Sylow theorems, free groups, permutation groups, and classification results.

InformationTheory

Entropy, Kullback-Leibler divergence, and information-theoretic inequalities.

LinearAlgebra

Matrices, bases, determinants, eigenvalues, bilinear forms, and the structure theorem for modules over a PID.

Logic

Propositional and first-order logic, model theory, and foundational set-theoretic constructions.

MeasureTheory

Sigma-algebras, Lebesgue and Bochner integration, Fubini, and Haar measure.

ModelTheory

First-order structures, satisfiability, the compactness theorem, and Löwenheim-Skolem.

NumberTheory

Primes, modular arithmetic, p-adic numbers, quadratic reciprocity, and algebraic number fields.

Order

Partial orders, lattices, complete lattices, Galois connections, and ordinal arithmetic.

Probability

Probability measures, independence, random variables, martingales, and limit theorems.

RepresentationTheory

Group representations, characters, orthogonality, and finite-dimensional representation categories.

RingTheory

Ideals, localizations, Dedekind domains, Witt vectors, and homological ring-theoretic results.

SetTheory

Ordinals, cardinals, aleph/beth numbers, cofinality, and a model of ZFC set theory.

Tactic

The Lean 4 tactic framework: ring, linarith, norm_num, simp, aesop, and hundreds more.

Testing

Infrastructure for property-based testing and linting used in Mathlib’s CI pipeline.

Topology

Topological spaces, filters, metric spaces, compactness, connectedness, and uniform spaces.

Util

Miscellaneous utilities and helper lemmas used across multiple domains.

​
Mathematical Coverage by Sub-page

Algebra

Groups, rings, fields, modules, linear algebra, polynomial rings, and Galois theory.

Analysis

Calculus, measure theory, functional analysis, and Fourier transforms.

Topology

Topological spaces, metric spaces, continuity, compactness, and filters.

Number Theory

Primes, modular arithmetic, p-adic numbers, and algebraic number fields.

Category Theory

Functors, adjunctions, limits, monoidal categories, and sheaves.

Other Areas

Combinatorics, probability, set theory, order theory, and more.

​
Scale and Scope

Mathlib is one of the largest formal mathematics libraries in the world. Its Mathlib.lean root file currently contains 8,234 import lines, each corresponding to a separately compiled module. The total codebase spans hundreds of thousands of lines of Lean 4 source.
Mathlib is actively maintained by a team of over 30 core maintainers and receives contributions from hundreds of mathematicians and computer scientists. The library’s coverage includes landmark results such as:
  • The structure theorem for finitely generated abelian groups (AddCommGroup.equiv_free_prod_directSum_zmod)
  • The Sylow theorems (Sylow.exists_subgroup_card_pow_prime)
  • Fubini’s theorem and the dominated convergence theorem for Bochner integrals
  • The Hahn-Banach theorem and Banach open mapping theorem
  • Quadratic reciprocity (legendreSym.quadratic_reciprocity)
  • The fundamental theorem of algebra via Complex.isAlgClosed
  • The Galois correspondence (IsGalois.intermediateFieldEquivSubgroup)
  • The strong law of large numbers and central limit theorem
To browse all covered theories interactively, visit the Mathlib overview page or the auto-generated API docs.

​
Using Mathlib

To use Mathlib in your own Lean 4 project, add it as a dependency in your lakefile.toml and import what you need: 
import Mathlib.Algebra.Group.Defs
import Mathlib.Topology.Basic
import Mathlib.NumberTheory.PrimeCounting

-- Or import everything at once:
import Mathlib
See the Installation guide for full setup instructions.

Build docs developers (and LLMs) love

Get started for freeTalk to us