Quickstart Guide: Write Your First Lean 4 Proof with Mathlib

This guide takes you from a blank file to a working collection of Lean 4 proofs using Mathlib. It assumes you have Lean 4 installed and a project with Mathlib as a dependency. If you have not done that yet, follow the Installation and Using Mathlib as a Dependency guides first. Once your project is set up and lake exe cache get has finished, you are ready to go — no further compilation is needed to run the examples below.

Your First Proof File

Inside your Lake project, create a new file called Proofs.lean at the root of the project (next to lakefile.lean). Every Lean file that uses Mathlib starts with an import:

Proofs.lean

import Mathlib

This single line makes every definition, theorem, and tactic in Mathlib available. For exploratory files this is always the right choice.

Exploring the Library with `#check`

Before writing proofs, it helps to know how to look things up. The #check command prints the type of any expression. Open Proofs.lean in VS Code, add the lines below, and hover over each #check to see the result in the Lean Infoview panel on the right:

Proofs.lean

import Mathlib

-- Lean prints the type (statement) of this theorem
#check Nat.exists_infinite_primes
-- Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ Nat.Prime p

#check Nat.add_comm
-- Nat.add_comm : ∀ (n m : ℕ), n + m = m + n

#check irrational_sqrt_two
-- irrational_sqrt_two : Irrational (√2)

In VS Code, placing your cursor on any identifier and pressing F12 jumps to the definition inside Mathlib. Use the Mathlib4 API docs search bar to discover theorems by keyword.

Example 1: Algebraic Identities with `ring`

The ring tactic proves equalities that hold in any commutative (semi)ring by normalising both sides. It handles polynomial identities over any ring type automatically — you never need to cite individual lemmas.

Proofs.lean

import Mathlib

-- Binomial expansion over the integers
example (a b : ℤ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

-- Difference of squares
example (a b : ℤ) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

-- Works over any CommRing, not just ℤ
example {R : Type*} [CommRing R] (x y z : R) :
    (x + y + z) ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + 2 * x * y + 2 * y * z + 2 * x * z := by
  ring

ring works over any type that carries a CommSemiring, CommRing, or compatible algebraic structure. It does not work for goals involving division or general field operations — use field_simp followed by ring in those cases.

Example 2: Linear Arithmetic with `linarith`

The linarith tactic discharges linear arithmetic goals over ordered fields and rings. It can combine hypotheses using linear combinations to close inequalities and contradictions.

Proofs.lean

import Mathlib

-- A basic inequality: if y > x > 0 then y > 0
example (x y : ℝ) (h1 : x > 0) (h2 : y > x) : y > 0 := by
  linarith

-- Combining multiple hypotheses
example (a b c : ℝ) (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ a + 1) : b ≤ a + 1 := by
  linarith

-- Deriving a contradiction from inconsistent hypotheses
example (x : ℝ) (h1 : x > 5) (h2 : x < 3) : False := by
  linarith

linarith only handles linear arithmetic. For nonlinear goals (e.g., x^2 ≥ 0), try nlinarith, positivity, or polyrith.

Example 3: Numeric Calculations with `norm_num`

The norm_num tactic evaluates numeric expressions and decides numeric propositions. It can verify primality, divisibility, inequalities between numeric literals, and much more — all by computation.

Proofs.lean

import Mathlib

-- Verify that 127 is prime
example : Nat.Prime 127 := by norm_num

-- A numeric inequality
example : (2 : ℝ) ^ 10 > 1000 := by norm_num

-- Divisibility
example : (12 : ℤ) ∣ 144 := by norm_num

-- Not prime
example : ¬ Nat.Prime 1 := by norm_num

Example 4: Using an Existing Mathlib Theorem

Mathlib contains hundreds of thousands of named theorems. Once you find one with #check, you can apply it directly in a proof using exact or apply.

Proofs.lean

import Mathlib

-- Mathlib already proves there are infinitely many primes.
-- We can simply reference the theorem.
#check Nat.exists_infinite_primes
-- Nat.exists_infinite_primes : ∀ (n : ℕ), ∃ p, n ≤ p ∧ Nat.Prime p

-- Use it to show there exists a prime larger than 100
example : ∃ p, 100 ≤ p ∧ Nat.Prime p := by
  exact Nat.exists_infinite_primes 100

-- Apply it as a step in a larger proof
example (n : ℕ) : ∃ p, n < p ∧ Nat.Prime p := by
  obtain ⟨p, hn, hp⟩ := Nat.exists_infinite_primes (n + 1)
  exact ⟨p, by linarith, hp⟩

Example 5: Combining Tactics

Real proofs often chain several tactics together. The by block is a sequenced tactic proof; each tactic transforms the current proof goal until it is closed.

Proofs.lean

import Mathlib

-- Prove that √2 is irrational using Mathlib's existing theorem
#check Nat.Prime.irrational_sqrt
-- Nat.Prime.irrational_sqrt : Nat.Prime p → Irrational (√↑p)

example : Irrational (Real.sqrt 2) := by
  have h : Nat.Prime 2 := by norm_num
  exact_mod_cast h.irrational_sqrt

-- A structured proof using `have` for intermediate steps
example (n : ℕ) (h : n > 0) : n * n > 0 := by
  have hn : n ≠ 0 := Nat.not_eq_zero_of_lt h
  exact Nat.mul_pos h h

Running Your File

Check in VS Code (recommended)

With the Lean 4 VS Code extension installed, simply open Proofs.lean. Lean checks the file incrementally as you type. The Lean Infoview panel (open with Ctrl+Shift+P → Lean 4: Show Infoview) displays the proof state at your cursor position, showing remaining goals and any error messages.

Check from the command line

To check a single file without the editor:

lean Proofs.lean

Lean prints any errors or warnings and exits. No output means all proofs are accepted.

Build the whole project

To compile every file in your Lake project:

lake build

Lake parallelises the build across your CPU cores. Because the Mathlib .olean cache is already present, only your own files need to be compiled.

Putting It All Together

Here is a complete, self-contained file you can drop into any Mathlib project and run immediately:

Proofs.lean

import Mathlib

/-!
# My First Mathlib Proofs

A small collection of proofs using Mathlib's core tactics.
-/

-- 1. Algebraic identity (ring)
example (a b : ℤ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by ring

-- 2. Linear arithmetic (linarith)
example (x y : ℝ) (h1 : x > 0) (h2 : y > x) : y > 0 := by linarith

-- 3. Numeric primality check (norm_num)
example : Nat.Prime 127 := by norm_num

-- 4. Infinitely many primes (exact application of a Mathlib theorem)
example : ∃ p, 100 ≤ p ∧ Nat.Prime p :=
  Nat.exists_infinite_primes 100

-- 5. A custom lemma with a structured tactic proof
lemma add_sq_nonneg (a b : ℝ) : (a - b) ^ 2 ≥ 0 := by positivity

The /-! ... -/ block at the top is a module docstring — Mathlib style encourages documenting every file this way. The text inside is rendered in the generated API docs.

Key Tactics Reference

Tactic	What it closes
`ring`	Polynomial identities in commutative (semi)rings
`linarith`	Linear arithmetic inequalities over ordered types
`nlinarith`	Nonlinear arithmetic inequalities
`norm_num`	Numeric computations, primality, divisibility
`decide`	Decidable propositions on finite/computable types
`simp`	Simplification using a set of rewrite rules
`aesop`	Automated proof search for structured goals
`omega`	Linear arithmetic over `ℕ` and `ℤ` specifically
`positivity`	Proves expressions are non-negative or positive
`exact`	Closes the goal with a provided term
`apply`	Applies a theorem, generating sub-goals for its hypotheses

Next Steps

Mathlib Tactics Overview

Full reference for all tactics available in Mathlib.

Mathematics in Lean

The community’s interactive textbook — the best structured introduction to proving mathematics in Lean.

Mathlib4 API Docs

Search for any theorem, definition, or tactic in Mathlib by name or type signature.

Lean Zulip Chat

Ask questions, share proofs, and discuss Mathlib with the community.

Getting Started

Mathematics

Tactics

Contributing

Quickstart Guide: Write Your First Lean 4 Proof with Mathlib

Your First Proof File

Exploring the Library with `#check`

Example 1: Algebraic Identities with `ring`

Example 2: Linear Arithmetic with `linarith`

Example 3: Numeric Calculations with `norm_num`

Example 4: Using an Existing Mathlib Theorem

Example 5: Combining Tactics

Running Your File

Putting It All Together

Key Tactics Reference

Next Steps

Mathlib Tactics Overview

Mathematics in Lean

Mathlib4 API Docs

Lean Zulip Chat

Build docs developers (and LLMs) love

Getting Started

Mathematics

Tactics

Contributing

Documentation Index

​Your First Proof File

​Exploring the Library with #check

​Example 1: Algebraic Identities with ring

​Example 2: Linear Arithmetic with linarith

​Example 3: Numeric Calculations with norm_num

​Example 4: Using an Existing Mathlib Theorem

​Example 5: Combining Tactics

​Running Your File

​Putting It All Together

​Key Tactics Reference

​Next Steps

Mathlib Tactics Overview

Mathematics in Lean

Mathlib4 API Docs

Lean Zulip Chat

Build docs developers (and LLMs) love

Your First Proof File

Exploring the Library with `#check`

Example 1: Algebraic Identities with `ring`

Example 2: Linear Arithmetic with `linarith`

Example 3: Numeric Calculations with `norm_num`

Example 4: Using an Existing Mathlib Theorem

Example 5: Combining Tactics

Running Your File

Putting It All Together

Key Tactics Reference

Next Steps