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. 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. Finding what you need in a million-line codebase used to be challenging, but the community has built excellent semantic search tools powered by AI, and the Mathlib documentation provides searchable API references for every declaration.

Core Foundations

These modules provide the logical and set-theoretic foundations that everything else depends on. The logic modules formalize propositional and predicate calculus, including both constructive reasoning and classical axioms like the law of excluded middle. Set theory in Mathlib is built on top of type theory rather than replacing it: Set α is defined as α → Prop, making sets predicates on types. This foundation supports finite sets with decidable membership, order theory including lattices and Galois connections, and the infrastructure for defining mathematical structures throughout the library.

Algebraic Hierarchy

Mathlib builds algebra through a hierarchy of type classes. Each structure adds operations and axioms to those below it. The hierarchy begins with semigroups and monoids, progresses through groups and rings, and culminates in fields and modules. This design means that a theorem about groups automatically applies to rings, fields, and any other structure that extends groups. The library includes both additive and multiplicative variants of each structure, connected by the @[to_additive] attribute that automatically generates parallel theories. Key accomplishments include complete formalizations of Galois theory, the structure theorem for finitely generated modules over PIDs, and the Nullstellensatz.

Number Systems

The standard number types and their properties, constructed with mathematical rigor. Natural numbers come from Lean’s core, but Mathlib adds comprehensive libraries for divisibility, primality, and arithmetic functions. Integers are built as a quotient of pairs of naturals. Rationals are fractions in lowest terms. Real numbers are equivalence classes of Cauchy sequences of rationals. Complex numbers are pairs of reals. Each construction comes with the expected algebraic structure and interoperability lemmas. The library also provides modular arithmetic through ZMod n, which is a field when n is prime.

Analysis and Topology

Continuous mathematics built on topological foundations. The topology library provides general topological spaces, filters, and nets as the foundation for limits and continuity. Metric spaces add distance functions with the expected triangle inequality and completeness properties. Analysis proper includes differentiation in arbitrary normed spaces, the Fréchet derivative for multivariable calculus, and integration via measure theory. Major formalizations include the Fundamental Theorem of Calculus, the Hahn-Banach theorem, the spectral theorem for compact self-adjoint operators, and the Central Limit Theorem. The library handles both real and complex analysis through a unified framework.

Category Theory and Combinatorics

Abstract structures and discrete mathematics form two largely independent branches of Mathlib. The category theory library provides a comprehensive framework for categorical reasoning: categories, functors, natural transformations, adjunctions, limits, colimits, and monads. This infrastructure supports both abstract mathematics and the categorical semantics of type theory. The combinatorics library covers graph theory with simple graphs and multigraphs, the pigeonhole principle, inclusion-exclusion, and generating functions. Notable formalizations include Szemerédi’s regularity lemma, the cap set problem bound, and significant progress toward the Polynomial Freiman-Ruzsa conjecture.

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. The community has built an ecosystem of search tools, each with different strengths.

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. Moogle uses embeddings trained on mathematical text, so it handles synonyms and related concepts well. 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. Loogle lets you search by the shape of the types involved, using wildcards and constraints. Precise queries get precise answers. This is the tool when you know the types but not the name.

LeanSearch: Another semantic search engine over Mathlib, focused on finding relevant theorems from natural language descriptions. It provides a different ranking algorithm than Moogle, so when one fails, try the other. Sometimes the theorem you need appears on page two of one engine and page one of another.

LeanExplore: Semantic search that indexes not just theorems but also metaprogramming, tactics, and attributes. It exposes an MCP (Model Context Protocol) interface, making it accessible to AI coding assistants. Useful when you need to find not just a lemma but how to use a particular tactic or attribute.

Lean Finder: Understands proof states and theorem statements at a deeper level than keyword matching. You can paste your current goal and it will suggest relevant lemmas. Particularly useful when you are mid-proof and need something that applies to your specific situation.

Mathlib4 Docs: The auto-generated API reference for every declaration in Mathlib. Not a search engine per se, but once you know the module, this is where you browse the available lemmas. Each declaration links to its source code and shows its type signature, docstring, and related definitions.

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 since they search locally compiled dependencies. Use them when web-based search fails or when you need something from a non-Mathlib dependency.

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.