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.

Lean 4 projects are managed by Lake, the official build system and package manager. Adding Mathlib to your project is a matter of declaring it as a dependency in your lakefile.lean, pinning the correct toolchain in lean-toolchain, and then fetching the precompiled .olean files so you do not have to compile Mathlib from scratch (a process that would take hours). This guide walks through every step.
These instructions assume you have already installed elan and Lean 4. If not, see the Installation guide first.

​
Creating a New Project

The fastest way to start is with Lake’s built-in math template, which scaffolds a project pre-configured to depend on Mathlib.
1

Create the project

Run the following command, replacing myproject with your desired project name:
lake new myproject math
cd myproject
Lake creates the following structure:
myproject/
├── lakefile.lean       # build configuration and dependencies
├── lean-toolchain      # pins the Lean version
├── lake-manifest.json  # locked dependency revisions (auto-generated)
└── Myproject.lean      # your first source file
2

Inspect the generated lakefile.lean

Open lakefile.lean. The math template generates a require statement that pulls in Mathlib from the leanprover-community GitHub organization:
lakefile.lean
import Lake
open Lake DSL

package myproject where
  name := "myproject"

require "leanprover-community" / "mathlib" @ git "master"

@[default_target]
lean_lib Myproject where
The require line tells Lake to fetch Mathlib from the master branch. Lake records the resolved commit hash in lake-manifest.json so builds are reproducible.
The lean-toolchain file generated by the template matches Mathlib’s current toolchain. Do not change this file manually unless you are intentionally upgrading to a newer Mathlib version.
3

Match the lean-toolchain file

Your project’s lean-toolchain must match the Lean version that Mathlib was built with. The template handles this automatically, but if you are adding Mathlib to an existing project, copy Mathlib’s toolchain version into your own lean-toolchain:
lean-toolchain
leanprover/lean4:v4.32.0-rc1
If your lean-toolchain does not match Mathlib’s, Lake will refuse to build and you will see toolchain mismatch errors. Always keep these files in sync.
4

Update dependencies

Fetch and lock the dependency tree:
lake update
This writes the resolved commit hash for Mathlib (and all its transitive dependencies) into lake-manifest.json. You should commit this file to version control so all collaborators use exactly the same library revisions.Mathlib’s own lakefile.lean includes a post_update hook that automatically runs lake exe cache get after lake update, provided the environment variable MATHLIB_NO_CACHE_ON_UPDATE is not set to 1. You will see output like:
Mathlib: fetching cache...
5

Fetch precompiled build cache

Mathlib contains hundreds of thousands of lines of Lean. Compiling it locally from source takes several hours. Instead, fetch the precompiled .olean files from Mathlib’s build cache server:
lake exe cache get
This downloads .olean files corresponding to the exact Mathlib commit in your lake-manifest.json. Typical download time is a few minutes depending on your connection.
If the cache download seems stale or something is mysteriously broken, try these recovery commands:
# Force re-download even if files exist locally
lake exe cache get!

# Or start fresh
lake clean
lake exe cache get
6

Build your project

With the cache in place, build your project:
lake build
Because the .olean files for Mathlib are already present, Lake only needs to compile your own source files, which takes seconds.

​
Adding Mathlib to an Existing Project

If you already have a Lake project and want to add Mathlib, edit your lakefile.lean to include the require statement:
lakefile.lean
import Lake
open Lake DSL

package myproject where
  name := "myproject"

-- Add this line:
require "leanprover-community" / "mathlib" @ git "master"

@[default_target]
lean_lib Myproject where
Then update your lean-toolchain file to match Mathlib’s version and run: 
lake update
lake exe cache get
lake build

​
Importing Mathlib in Your Source Files

Once Mathlib is a declared dependency and the cache has been fetched, you can import it in any .lean file.

​
Import Everything

For exploratory work or small projects, import the entire library with a single line: 
import Mathlib
This makes all of Mathlib’s definitions, lemmas, and tactics available. It is the simplest approach, though it does increase the initial compilation time for your file.

​
Selective Imports

For larger projects where compilation time matters, import only the modules you need: 
-- Just group theory
import Mathlib.Algebra.Group.Defs

-- Just natural number basics
import Mathlib.Data.Nat.Basic

-- Prime number theory
import Mathlib.Data.Nat.Prime.Basic

-- The `ring` tactic
import Mathlib.Tactic.Ring
Not sure which module defines something? Use the Mathlib4 API docs search bar or the #check command in VS Code to find the source location of any declaration.

​
The post_update Hook and Cache Automation

Mathlib ships a post_update script in its own lakefile.lean. When you run lake update in a downstream project (i.e., any project that depends on Mathlib), Lake automatically invokes this hook. The hook:
  1. Checks that the running Lake version matches the toolchain version in lean-toolchain.
  2. If they match, runs lake exe cache get automatically.
  3. If they do not match (e.g., you have just changed the toolchain), it prints a message asking you to run lake exe cache get manually.
This means that for most day-to-day workflows, simply running lake update is enough — the cache is fetched for you.

​
Disabling Automatic Cache Fetch

If you are in an environment where the cache should not be fetched automatically (e.g., a CI job that manages caching separately), set the following environment variable before running lake update: 
export MATHLIB_NO_CACHE_ON_UPDATE=1
lake update
With this variable set, the post_update hook exits early and no cache download is attempted.

​
Minimal Working lakefile.lean

Here is a complete, minimal lakefile.lean for a downstream project that depends on Mathlib:
lakefile.lean
import Lake
open Lake DSL

package «myproject» where
  name := "myproject"

require "leanprover-community" / "mathlib" @ git "master"

@[default_target]
lean_lib «Myproject» where
And the accompanying lean-toolchain:
lean-toolchain
leanprover/lean4:v4.32.0-rc1

​
Updating Mathlib

To update to the latest Mathlib revision, run: 
lake update
This updates lake-manifest.json to the latest master commit, updates lean-toolchain if necessary, and (via the post_update hook) fetches fresh cache files.
Updating Mathlib may change the required Lean toolchain version. Always review the updated lean-toolchain file and ensure your team is using the matching elan toolchain.

​
Transitive Dependencies

When you depend on Mathlib, you automatically inherit its transitive dependencies. These are all managed by Lake and recorded in lake-manifest.json. The current set includes:
PackagePurpose
batteriesExtended standard library and basic tactics
aesopAutomated proof search tactic
QqTyped metaprogramming quotations
proofwidgetsInteractive UI widgets for the infoview
importGraphImport graph analysis utilities
LeanSearchClientIntegration with Lean search services
plausibleProperty-based testing for Lean
You do not need to declare these separately — they are pulled in transitively through Mathlib.

​
Next Steps

With Mathlib installed and imported, you are ready to start writing proofs. Head to the Quickstart guide to see real working examples using Mathlib’s most useful tactics.

Build docs developers (and LLMs) love

Get started for freeTalk to us