Lean4
Module 5 · Lesson 1

Introduction to Mathlib

Mathlib is the community mathematics library for Lean 4. It adds definitions and theorems across most of undergraduate mathematics and beyond, plus tactics such as ring and linarith.

❗
The tactics in this module require Mathlib4. They are not part of core Lean 4 and must be imported from the Mathlib library.

What is Mathlib?

Mathlib is a community-driven mathematical library containing:

  • Over a million lines of formalized mathematics
  • Algebra, analysis, topology, number theory, and more
  • Powerful automation tactics for common proof patterns
  • Type class hierarchies for abstract mathematics

Setting Up Mathlib

The quickest start is a new project from Lake's math template, which already depends on Mathlib:

bash
1lake new my_project math
2cd my_project
3lake exe cache get   # download prebuilt Mathlib instead of compiling it
4lake build

To add Mathlib to an existing project, declare it in lakefile.toml:

toml
1[[require]]
2name = "mathlib"
3scope = "leanprover-community"

or, in a lakefile.lean:

lean
1require mathlib from git
2  "https://github.com/leanprover-community/mathlib4"

Then run lake update and lake exe cache get. Without the cache, Lake compiles all of Mathlib from source, which takes hours. Run lake exe cache get again whenever you update Mathlib.

lean
1-- In your Lean files:
2import Mathlib.Tactic  -- Import all tactics
3
4-- Or import specific modules:
5import Mathlib.Tactic.Ring
6import Mathlib.Tactic.Linarith
7import Mathlib.Tactic.FieldSimp
Key Takeaway
Mathlib tactics must be imported before use. The importMathlib.Tactic brings in all common tactics.

Finding a Lemma in Mathlib

Mathlib has hundreds of thousands of lemmas, so the usual question is not whether a fact is proved but what it is called. Lean can search for you from inside a proof:

lean
1example (a b : ℕ) : a + b = b + a := by
2  exact?   -- suggests: exact Nat.add_comm a b
3
4example (a b c : ℝ) (h : a ≤ b) (hc : 0 ≤ c) : a * c ≤ b * c := by
5  apply?   -- lists lemmas whose conclusion fits, such as mul_le_mul_of_nonneg_right

exact? looks for a single lemma that closes the goal, apply? for lemmas whose conclusion matches it, and rw? for equations that rewrite it. Outside a proof, search by type shape with Loogle, or by name in the Mathlib documentation. Names follow the statement: mul_le_mul_of_nonneg_right says "multiply both sides of a ≤ on the right by a nonnegative number", so once you know the convention you can often guess a name and confirm it with #check.

Core Lean 4 vs Mathlib Tactics

lean
1-- Core Lean 4 tactics (always available):
2-- rfl, rw, simp, exact, apply, intro, cases, induction
3-- constructor, have, let, omega, decide, native_decide
4
5-- Mathlib tactics (require import):
6-- ring, field_simp, linarith, nlinarith, polyrith
7-- rcases, obtain, push_neg, contrapose, ext, congr
8-- norm_num, positivity, gcongr, and many more

Why Use Mathlib Tactics?

1. Domain-Specific Automation

lean
1import Mathlib.Tactic.Ring
2
3-- ring solves polynomial equations automatically
4example (x y : Int) : (x + y)^2 = x^2 + 2*x*y + y^2 := by ring
5
6-- Without ring, this requires many rewrites!

2. Proof Search

lean
1import Mathlib.Tactic.Linarith
2
3-- linarith finds linear arithmetic contradictions
4example (x y : Int) (h1 : x < y) (h2 : y < x) : False := by linarith
5
6-- It searches through hypotheses automatically

3. Structural Tactics

lean
1import Mathlib.Tactic.Cases
2
3-- rcases provides powerful pattern matching
4example (h : ∃ n : Nat, n > 0 ∧ n < 10) : True := by
5  rcases h with ⟨n, hn_pos, hn_lt⟩
6  trivial
Deep Dive: Mathlib's Philosophy

Mathlib follows several design principles:

  • Generality: Define concepts at their most general level
  • Bundling: Group related structures together
  • Automation: Provide tactics that handle routine proofs
  • Consistency: Follow naming conventions strictly

Mathlib Tactics in This Module

We'll cover the most commonly used Mathlib tactics:

Arithmetic Tactics

  • ring — Solve polynomial ring equations
  • field_simp — Simplify field expressions with division
  • linarith — Linear arithmetic reasoning
  • nlinarith — Nonlinear arithmetic
  • polyrith — Polynomial arithmetic search

Structural Tactics

  • rcases / obtain — Pattern matching
  • push_neg — Push negations inward
  • contrapose — Contrapositive reasoning
  • ext — Extensionality
  • congr — Congruence

Getting Started

lean
1-- Quick setup with all Mathlib tactics:
2import Mathlib.Tactic
3
4-- Now you can use ring, linarith, and more!
5example (a b : ℤ) : (a - b) * (a + b) = a^2 - b^2 := by ring
💡
Start with import Mathlib.Tactic to get all tactics. Later, you can import only what you need for faster compilation.
Exercise: Import and Use ring

Import Mathlib tactics and use ring on a simple identity.

lean
1import Mathlib.Tactic
2
3example (x : Int) : (x + 1)^2 = x^2 + 2*x + 1 := by
4  ring
Custom TacticsNext: ring