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 community tracks progress against a list of 100 major theorems; most are done.

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.

Moogle: Semantic search for Mathlib. Type “triangle inequality for norms” and find norm_add_le. Sometimes it even understands what you meant rather than what you typed. Start here when you know what you want but not what it is called.

Loogle: Type signature search. If you need a lemma involving List.map and List.length, search for List.map, List.length and find List.length_map. Precise queries get precise answers.

In-editor tactics: The exact? tactic searches for lemmas that exactly match your goal. The apply? tactic finds lemmas whose conclusion unifies with your goal. Slow but thorough. Use them when Moogle and Loogle fail.

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

The Fundamental Theorem of Calculus in Mathlib is due to Yury Kudryashov and Benjamin Davidson. It comes in two parts, as you might remember from analysis.

The first part says that integrating then differentiating recovers the original function. If \(f\) is integrable and tends to \(c\) at \(b\), then the function \(u \mapsto \int_a^u f(x),dx\) has derivative \(c\) at \(b\):

theorem integral_hasStrictDerivAt_of_tendsto_ae_right
    (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (nhds b) volume)
    (hb : Tendsto f (nhds b ⊓ ae volume) (nhds c)) :
    HasStrictDerivAt (fun u => ∫ x in a..u, f x) c b

The second part says that differentiating then integrating recovers the original function up to boundary values. If \(f\) is continuous on \([a,b]\) and differentiable on \((a,b)\) with integrable derivative, then:

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

theorem integral_eq_sub_of_hasDeriv_right_of_le
    (hab : a ≤ b)
    (hcont : ContinuousOn f (Icc a b))
    (hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt f (f' x) (Ioi x) x)
    (hint : IntervalIntegrable f' volume a b) :
    ∫ x in a..b, f' x = f b - f a

The hypotheses handle the edge cases your calculus teacher glossed over: continuity on the closed interval, differentiability on the open interior, integrability of the derivative. Centuries of refinement, machine-checked.

Resources

• Moogle - Search Mathlib using natural language queries like “triangle inequality for norms”.
• Loogle - Search by type signature when you know the shape of the lemma you need.
• LeanSearch - Semantic search over Mathlib with a focus on finding relevant theorems.
• LeanExplore - Semantic search that also indexes metaprogramming and exposes an MCP interface for AI agents.
• Lean Finder - Understands proof states and theorem statements, not just keywords.
• Mathlib4 Docs - Auto-generated API reference for every declaration in Mathlib.
• Mathematics in Mathlib - Map of formalized mathematics organized by mathematical area.
• 100 Theorems - Tracks which of 100 major theorems have been formalized in Lean.
• Zulip Chat - Ask questions in the “Is there code for X?” stream when search engines fail.
• GitHub - Source code, issue tracker, and contribution guidelines.