Mathlib

Mathlib is the mathematical library for Lean 4. Over a million lines of formalized mathematics, from basic logic through graduate-level algebra, analysis, and number theory. Hundreds of contributors have poured years of work into this thing. When you import it, you inherit their labor. The triangle inequality is already proven. So is the fundamental theorem of algebra. You do not need to prove that primes are infinite; someone did that in 2017 and you can just use it.

The library is organized hierarchically, which is a polite way of saying “good luck finding anything without help.” At the foundation sit logic, sets, and basic data types. Above these rise algebraic structures, then topology and analysis, then specialized domains like combinatorics and number theory. Each layer builds on those below. The Mathlib documentation provides searchable API references, though “searchable” is doing some heavy lifting in that sentence.

Core Foundations

These modules provide the logical and set-theoretic foundations that everything else depends on.

Algebraic Hierarchy

Mathlib builds algebra through a hierarchy of type classes. Each structure adds operations and axioms to those below it.

Number Systems

The standard number types and their properties.

Analysis and Topology

Continuous mathematics built on topological foundations.

Category Theory and Combinatorics

Abstract structures and discrete mathematics.

Finding What You Need

Mathlib is large. You will spend more time searching for lemmas than proving theorems, at least at first. Accept this. The good news is that the lemma you need almost certainly exists. The bad news is that it might be named something you would never guess.

In-editor search: The exact? tactic searches for lemmas that exactly match your goal. The apply? tactic finds lemmas whose conclusion unifies with your goal. These are your best friends. Use them constantly.

Pattern search: Loogle searches Mathlib by type signature. If you need a lemma about List.map and List.length, search for List.map, List.length and find List.length_map. This works better than it sounds.

Natural language search: Moogle uses semantic search to find lemmas from natural language queries. Ask “triangle inequality for norms” and find norm_add_le. Sometimes it even understands what you meant rather than what you typed.

Module structure: If you need facts about prime numbers, look in Mathlib.Data.Nat.Prime. If you need topology lemmas, start in Mathlib.Topology. The Mathematics in Mathlib overview provides a map of what has been formalized and where. When all else fails, grep the source code like everyone else does.

Importing Mathlib

Most projects import Mathlib wholesale:

import Mathlib

This works, but your compile times will make you reconsider your life choices. For faster iteration during development, import only what you need:

-- Import specific modules for faster compilation
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Group.Basic
import Mathlib.Tactic

The Mathlib documentation lists all available modules. When your proof needs a specific lemma, check which module provides it and add that import. Or just import everything and go make coffee while it compiles.

Working with Primes

Number theory in Mathlib is surprisingly pleasant. The basics are all there, and the proofs often look like what you would write on paper if paper could check your work:

-- Working with prime numbers from Mathlib
example : Nat.Prime 17 := by decide

example : ¬ Nat.Prime 15 := by decide

-- Every number > 1 has a prime factor
example (n : Nat) (h : n > 1) : ∃ p, Nat.Prime p ∧ p ∣ n := by
  have hn : n ≠ 1 := by omega
  exact Nat.exists_prime_and_dvd hn

-- Infinitely many primes: for any n, there's a prime ≥ n
example (n : Nat) : ∃ p, Nat.Prime p ∧ p ≥ n := by
  obtain ⟨p, hn, hp⟩ := Nat.exists_infinite_primes n
  exact ⟨p, hp, hn⟩

Algebraic Structures

Type classes do the heavy lifting here. Declare that your type is a group, and you get inverses, identity laws, and associativity for free. Declare it is a ring, and multiplication distributes over addition without you lifting a finger:

-- Using algebraic structures

-- Groups: every element has an inverse
example {G : Type*} [Group G] (a : G) : a * a⁻¹ = 1 :=
  mul_inv_cancel a

-- Rings: distributivity comes for free
example {R : Type*} [Ring R] (a b c : R) : a * (b + c) = a * b + a * c :=
  mul_add a b c

-- Commutativity in commutative rings
example {R : Type*} [CommRing R] (a b : R) : a * b = b * a :=
  mul_comm a b

Real Numbers

The reals are constructed as equivalence classes of Cauchy sequences, which is mathematically clean but occasionally leaks through the abstraction when you least expect it. Most of the time you can pretend they are just numbers:

-- Real number analysis

-- Reals are a field
example (x : ℝ) (h : x ≠ 0) : x * x⁻¹ = 1 :=
  mul_inv_cancel₀ h

-- Basic inequalities
example (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 0 < x + y :=
  add_pos hx hy

-- The triangle inequality
example (x y : ℝ) : |x + y| ≤ |x| + |y| :=
  abs_add_le x y

Mathlib Tactics

Mathlib ships tactics that know more mathematics than most undergraduates. ring closes polynomial identities. linarith handles linear arithmetic over ordered rings. positivity proves things are positive. These are not magic; they are carefully engineered decision procedures. But from the outside, they look like magic:

-- Mathlib tactics in action

-- ring solves polynomial identities
example (x y : ℤ) : (x - y) * (x + y) = x^2 - y^2 := by ring

-- linarith handles linear arithmetic
example (x y z : ℚ) (h1 : x < y) (h2 : y < z) : x < z := by linarith

-- field_simp clears denominators
example (x : ℚ) (h : x ≠ 0) : (1 / x) * x = 1 := by field_simp

-- positivity proves positivity goals
example (x : ℝ) : 0 ≤ x^2 := by positivity

-- gcongr for monotonic reasoning
example (a b c d : ℕ) (h1 : a ≤ b) (h2 : c ≤ d) : a + c ≤ b + d := by gcongr

Using Search Tools

When stuck, let the computer do the searching. exact? trawls through Mathlib looking for a lemma that exactly matches your goal. apply? finds lemmas whose conclusion fits. These tactics are slow, but they beat staring at the screen trying to remember if the lemma is called add_comm or comm_add:

-- Finding lemmas with exact? and apply?

-- When stuck, use exact? to find matching lemmas
example (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n  -- exact? would suggest this

-- apply? finds lemmas whose conclusion matches goal
example (a b : Nat) (h : a ∣ b) (h2 : b ∣ a) : a = b := by
  exact Nat.dvd_antisymm h h2  -- apply? would find this

The Fundamental Theorem of Calculus

Remember the Fundamental Theorem of Calculus from high school? The one that says the integral of a derivative gives you back the original function, evaluated at the endpoints? That theorem you memorized, used on exams, and maybe wondered if it was actually true or just something teachers said?

$$\int_a^b f’(x) , dx = f(b) - f(a)$$

It is proven in Mathlib. All of it. This statement is a theorem you can import and use. The proof handles all the edge cases your calculus teacher glossed over: measurability, integrability, what happens at the boundary points. Centuries of mathematical refinement, compressed into something a computer can check.

import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

open MeasureTheory Set

-- The second fundamental theorem of calculus: ∫ f' = f(b) - f(a)
example (f f' : ℝ → ℝ) (a b : ℝ)
    (hf : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
    (hf' : IntervalIntegrable f' volume a b) :
    ∫ x in a..b, f' x = f b - f a :=
  intervalIntegral.integral_eq_sub_of_hasDerivAt hf hf'

That is high school calculus, machine-verified. The gap between “this seems true” and “this is proven” turns out to be about four lines of Lean.