Getting started — up to checking a single file

You do not need to install Lean itself directly. The only thing you install is elan (it comes via the installation script that Lean's official distributor provides), and it switches Lean versions for you.

Knowing how it works keeps you from getting lost. At the top of a project there is a one-line file called lean-toolchain.

leanprover/lean4:v4.33.1

When you call lean or lake in that directory, elan reads this line, fetches that version automatically if needed, and uses it. Even if different projects need different versions, there is never a manual switching step.

A project that uses mathlib is heavy. The Lean version itself takes about 3 GB of disk, and the prebuilt artifacts of mathlib about 9 GB. For memory, depending on what is in the proofs, allow 4 GB to 16 GB.

When something does not work, the first thing to ask is the version.

elan --version
lean --version
lake --version

In the environment where every snippet in this guide was checked, this is the output.

elan 4.2.4 (227caca13 2026-08-25)
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
Lake version 5.0.0-src+819816b (Lean version 4.33.1)

The version of mathlib does not appear in lean --version. The project's lake-manifest.json records, for each dependency, where it was fetched from and which revision. In this environment it is as follows.

This revision value is the real key to reproducing a result. "Checked in Lean 4" is not enough. In mathlib both the names of lemmas and the definitions move, so the same source may fail to pass half a year later. Distribute lake-manifest.json along with it, and that is pinned.

myproject/
├── lakefile.toml        package name, dependencies, options
├── lake-manifest.json   pins the revision of each dependency (written by lake)
├── lean-toolchain       the Lean version (read by elan)
├── Foo.lean             entry point of the library; it just imports and lists Foo/
├── Foo/
│   ├── Bar.lean         the contents
│   └── Baz.lean
└── .lake/               where fetched packages and build results go (do not touch by hand)

lakefile.toml can be short.

name = "myproject"
version = "0.1.0"
defaultTargets = ["Foo"]

[leanOptions]
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.33.1"

[[lean_lib]]
name = "Foo"

relaxedAutoImplicit = false is worth putting in. If you leave this relaxed, a misspelled identifier is silently accepted as an implicit type variable, and a proposition with a different meaning passes the check.

The first time you fetch the dependencies, building mathlib from source takes several hours. Fetching the prebuilt artifacts takes minutes.

lake exe cache get

What this fetches is the olean files — intermediate files holding the checked declarations, which are what gets read at import.

To check just one file, this is it.

lake env lean Foo/Bar.lean

lake env sets up environment variables for where the project's dependencies live (such as the path for finding mathlib's olean files) and then runs the command that follows. That is why you use lake env lean rather than calling lean directly.

For example, check the following file.

import Mathlib

theorem add_self_even (n : ℕ) : 2 ∣ n + n := ⟨n, by ring⟩

The output is empty. That means "it passed". Lean does not report success. The exit code is 0, and 1 if there is an error. Until you get used to this silence it is unsettling, but empty output is strong information — every declaration that needed checking passed the type check, and not a single warning was raised.

There is just one difference between lake env lean and lake build.

In a project with heavy proofs, lake build by default builds as many files at once as there are CPUs. If a single proof uses several GB, that alone can exhaust memory and leave you in a state that neither crashes nor progresses. In that case, limit the concurrency with LEAN_NUM_THREADS.

Type mismatch

example (a b : ℕ) : a + b = b + a := Nat.add_comm b a

3:37: error: Type mismatch
  Nat.add_comm b a
has type
  b + a = a + b
but is expected to have type
  a + b = b + a

Line 3, column 37; the term written was Nat.add_comm b a; its type is b + a = a + b; the type required is a + b = b + a. The arguments were in the wrong order. Change it to Nat.add_comm a b and it passes.

"Type mismatch" is not a report that the proposition is false. It only says that the term you handed over has a different shape from the hole you are trying to fill. Comparing the two lines has type and but is expected to have type is how to read this kind of error.

unsolved goals

theorem zero_both (n : ℕ) : n + 0 = n ∧ 0 + n = n := by
  constructor
  · rfl

3:53: error: unsolved goals
case right
n : ℕ
⊢ 0 + n = n

Read it in three steps. case right is the name of the branch left unclosed — constructor split the conjunction into two, left and right, and the branch begun with · closed only the left, so the right remains. Below it, n : ℕ is what is available at that point. To the right of ⊢ is the proposition to be shown.

The position points at the end of line 3 (the by) because this is a report that the proof as a whole has goals remaining, not about any individual tactic.

A small lesson is buried here. The left branch closes with rfl, but the right one does not. Addition on natural numbers is defined by recursion on the second argument, so n + 0 becomes n just by unfolding the definition, but 0 + n does not. The right side needs simp or Nat.zero_add. Something that looks symmetric on paper is not symmetric at the level of definitions — the first step that trips up anyone who starts writing in Lean.

#check two_add_two
#check Nat.add_comm
#check (2 + 2 : ℕ)
#eval 2 + 2
#eval (List.range 10).map (· ^ 2)

two_add_two : 2 + 2 = 4
Nat.add_comm (n m : ℕ) : n + m = m + n
2 + 2 : ℕ
4
[0, 1, 4, 9, 16, 25, 36, 49, 64, 81]

The result of #eval is not a proof. It is a value evaluated by compiled code, and has not gone through the kernel. It is a tool for confirming, after writing a definition, "does the value I expected come out?", and carries the same weight as the computation label. To make a value into a claim, rewrite the same thing with decide or an explicit proof.

mathlib is a collection of more than 8,000 files. There are four roads to finding the lemma you need.

Finding a lemma that closes the goal outright — exact?

example (a b : ℕ) : a + b = b + a := by exact?

Try this:
  [apply] exact Nat.add_comm a b

Combining hypotheses to hit the goal — apply?

example (a b c : ℕ) (h : a ≤ b) (h2 : b ≤ c) : a ≤ c := by apply?

Try this:
  [apply] exact Nat.le_trans h h2

In both cases, copy the term that was found and put it in place as is. Do not leave exact? in a proof — the search runs every time, which slows the check, and the result changes when mathlib moves.

Grepping the source

The fetched mathlib is placed under .lake/packages/mathlib/. If you can remember part of the name, picking out just the declaration lines is fast.

grep -rnE "^(lemma|theorem) card_le_card_of_inj" .lake/packages/mathlib/Mathlib/

.lake/packages/mathlib/Mathlib/Data/Finset/Card.lean:427:lemma card_le_card_of_injOn (f : α → β) (hf : Set.MapsTo f s t) (f_inj : (s : Set α).InjOn f) :
.lake/packages/mathlib/Mathlib/Data/Finset/Card.lean:434:lemma card_le_card_of_injective {f : s → t} (hf : f.Injective) : #s ≤ #t := by
.lake/packages/mathlib/Mathlib/SetTheory/Cardinal/Finite.lean:94:lemma card_le_card_of_injective {α : Type u} {β : Type v} [Finite β] (f : α → β)
.lake/packages/mathlib/Mathlib/SetTheory/Cardinal/Finite.lean:316:lemma card_le_card_of_injective {α β : Type*} {f : α → β} (hf : Injective f) : card α ≤ card β := by

Note that the same name appears again and again in different namespaces. The one for Finset, the one for Nat.card, and the one for cardinals differ in both hypotheses and conclusion. Once grep has given you a candidate, confirm the statement with #check @thatname.

Working backwards from the name to the spelling

mathlib names are the conclusion read out in English words. Once you know this correspondence, you can guess the name before searching.

The direction of reading is "conclusion _of_ hypothesis". Nat.eq_one_of_dvd_one is "equal to 1 if it divides 1" —

#check @Nat.eq_one_of_dvd_one

@Nat.eq_one_of_dvd_one : ∀ {n : ℕ}, n ∣ 1 → n = 1

Just as read. Conversely, if you translate the expression you want to show into the spellings add, le, comm before searching, you hit the target sooner.

For the claims in this site's articles that carry the Lean label, the complete sources are distributed. The procedure, the memory needed, the ledger of theorems, and the list of axioms relied on are in The Lean verification bundle.

A one-step way to run it is provided, but what is inside is the same as what we saw above — use the lake-manifest.json with pinned dependencies, fetch mathlib's olean files with lake exe cache get, build in order with lake build, and finally list the output of #print axioms. If the results disagree, that is what we want to know. The contact address is on that page.

Sources and reproduction

Next: 03 Handing a finite check to decide — the first hands-on example. Terms are in 12 Glossary.