Introduction

Who it is for. This guide is aimed at teachers who want to introduce Lean 4 to mathematics students who are used to writing proofs on paper but have no previous programming experience. No prior knowledge of computer science is required.

Philosophy of the course.

1. Lean is a proof notebook that talks back. You write an argument and the computer tells you, step by step, what is missing. It is presented as a patient interlocutor, not as a programming language.
2. Mathematics first, syntax later. Each topic starts from a proof the student already knows how to do on paper and translates it into Lean.
3. No installation at the beginning. The first three sessions can be done in the browser. Local installation comes when the student already wants to carry on alone.
4. You learn by reading the proof state. The central skill is not memorizing tactics, but reading the goals window (the infoview) the way one reads a blackboard.
5. Making mistakes is cheap. The red error is information, not a failure.

Structure. Eight topics of about 2 hours each (theory and practice mixed). Each topic has two parts: the content (what the student sees) and the teaching tips (notes for the teacher with key ideas, typical mistakes, ...).

Convention. All the examples start with import Mathlib.Tactic, Lean's library of tactics. The code blocks can be pasted as they are into the editor.

Topic 1. First contact

Content

Objectives. Open Lean, write a statement, read the proof state and close a very simple proof.

1.1 What Lean is (in three sentences). Lean is a proof assistant: it checks that every step of an argument is logically correct. Statements are written in a language very close to the mathematical one. A proof accepted by Lean has no gaps.

1.2 Where to write. To start, the Lean web editor is enough. You write on the left; on the right appears the infoview, which shows what Lean answers. To work locally, use Visual Studio Code with the Lean 4 extension, which guides the installation.

1.3 Your first statement

import Mathlib.Tactic

example : 2 + 2 = 4 :=
by norm_num

Reading: “Example: 2 + 2 = 4. Proof: compute with norm_num.” The word example introduces an unnamed statement; by announces that we are going to prove with tactics, which are commands of the kind “apply this result”, “compute”, “split into cases”.

1.4 Hypotheses and goal. Place the cursor after by in the following example:

example
  (a b : ℕ)
  (h : a = b)
  : b = a :=
by
  exact h.symm

The infoview shows:

a b : ℕ
h : a = b
⊢ b = a

Above the ⊢ line are the hypotheses (what we have); after ⊢ is the goal (what we want). The whole technique of Lean consists in transforming the goal until it is closed. exact h.symm says: “the goal is obtained exactly from h by turning it around”.

1.5 Named theorems.

theorem my_add_comm
  (a b : ℕ)
  : a + b = b + a :=
by
  exact Nat.add_comm a b

theorem my_add_comm'
  (a b : ℕ)
  : a + b = b + a :=
by
  ring

ℕ is typed \N and the editor converts it automatically; likewise \R for ℝ, \to for →, \forall for ∀, \ex for ∃. Two proofs of the same fact: one citing a lemma, the other computing. Both are valid.

1.6 The underlying idea, without drama. In Lean, statements are types and proofs are elements of those types. You do not need to understand type theory to start: it is enough to know that h : a = b means “h is a proof that a = b” and that it is used like any other piece of data.

Exercises.

1. Prove

    example
      (a b c : ℕ)
      (h1 : a = b)
      (h2 : b = c)
      : a = c

with `exact h1.trans h2`.

1. Prove

    example
      (x : ℝ)
      : x + 0 = x

with `ring`, and then with `exact add_zero x`.

1. Change the statement of my_add_comm to something false (for example a + b = b + a + 1) and read the error. What does Lean tell you is missing?
2. Put sorry in place of a proof. What difference is there in the color and in the message?

Teaching tips

• Idea that must be clear. The infoview is the blackboard. If the student gets lost, the answer is almost always “look at the goal”.
• How to present it. Start with a paper proof of a = b → b = a and do it in parallel in Lean. The student must see that the reasoning is the same.
• Common mistakes.
  • Forgetting import Mathlib.Tactic.
  • Typing ASCII (->) and not understanding why it changes: both are valid, but it is best to stick to one.
  • Indentation: after by, the lines must be indented and aligned.
  • Confusing = with :=.
• On type theory. Keep the discourse to a minimum. If they ask, answer briefly and postpone the discussion to Topic 6.
• A trick to remove fear. Let them break things on purpose. A Lean error is almost never serious, and seeing one early works like a vaccine.

Topic 2. Propositional logic

Content

Objectives. Handle →, ∧, ∨, ¬, ↔ with the basic tactics. Each connective has one way to construct it and another to use it.

2.1 Propositions. P Q : Prop declares two arbitrary propositions. A hypothesis hP : P says that P is true.

2.2 Table of tactics.

2.3 Examples.

example
  (P Q : Prop)
  : P ∧ Q → Q ∧ P :=
by
  intro h
  -- h : P ∧ Q
  -- ⊢ Q ∧ P
  obtain ⟨hp, hq⟩ := h
  -- hp : P
  -- hq : Q
  exact ⟨hq, hp⟩

example
  (P Q : Prop)
  (hP : P)
  (hQ : Q)
  : P ∧ Q :=
by
  constructor
  · -- ⊢ P
    exact hP
  · -- ⊢ Q
    exact hQ

example
  (P Q : Prop)
  : P ∨ Q → Q ∨ P :=
by
  intro h
  -- h : P ∨ Q
  -- ⊢ Q ∨ P
  rcases h with hp | hq
  · -- hp : P
    right
    -- ⊢ P
    exact hp
  · -- hq : Q
    left
    -- ⊢ Q
    exact hq

example
  (P Q : Prop)
  (h : P → Q)
  (hnq : ¬ Q)
  : ¬ P :=
by
  intro hp
  -- hp : P
  -- ⊢ False
  exact hnq (h hp)

After each step I have annotated, as a comment starting with --, the changes that step produces in the hypotheses or in the goal. These comments are optional and are not part of the proof.

The dot · opens a subgoal: after constructor there are two goals and each dot deals with one of them.

2.4 Mathematical reading. The first example is “suppose P and Q; then we have Q and P”. intro is suppose; obtain is let us decompose the hypothesis; exact is we conclude.

Exercises.

1. P ∧ (Q ∧ R) → (P ∧ Q) ∧ R.
2. (P → Q) → (Q → R) → (P → R).
3. P ∨ Q → (P → R) → (Q → R) → R.
4. ¬ (P ∧ ¬ P).
5. Challenge: (P ↔ Q) → (Q ↔ P).

Teaching tips

• Strategy. Always present the construct / use pair. It is the common thread of the whole course and it will reappear with ∀ and ∃.
• Common mistakes.
  • Trying exact when an intro is missing.
  • Not seeing that ¬ P is P → False.
  • Forgetting the dot · or indenting it badly; Lean warns with “unsolved goals”.
• Useful resource. Teach assumption (closes the goal if it matches a hypothesis) and tauto (solves tautologies) only after they have done the exercises by hand. Otherwise tauto defeats the learning.
• Classical logic. Mathlib is classical: by_contra, by_cases and push_neg are available. Mention it without going into constructivism, unless the group asks for it.

Topic 3. Quantifiers and sets

Content

Objectives. Use ∀ and ∃, and work with sets through membership, inclusion and equality by double inclusion.

3.1 Quantifiers. They follow the same construct / use pattern.

example : ∃ n : ℕ, n * n = 16 :=
by
  use 4

example
  (f : ℝ → ℝ)
  (hf : ∀ x, f x = 2 * x + 1)
  : f 3 = 7 :=
by
  rw [hf]
  -- ⊢ 2 * 3 + 1 = 7
  norm_num

example
  (P : ℕ → Prop)
  (h : ∃ n, P n)
  : ¬ ∀ n, ¬ P n :=
by
  intro h1
  -- h1 : ∀ (n : ℕ), ¬P n
  -- ⊢ False
  obtain ⟨n, hn⟩ := h
  -- n : ℕ
  -- hn : P n
  exact h1 n hn

3.2 Sets. Set ℕ is the type of subsets of ℕ. x ∈ A ∩ B is, by definition, x ∈ A ∧ x ∈ B, so the tactics from Topic 2 work directly.

example
  (A B : Set ℕ)
  : A ∩ B ⊆ A :=
by
  intro x hx
  -- x : ℕ
  -- hx : x ∈ A ∩ B
  -- ⊢ x ∈ A
  exact hx.1

example
  (A B : Set ℕ)
  : A ∩ B = B ∩ A :=
by
  ext x
  -- ⊢ x ∈ A ∩ B ↔ x ∈ B ∩ A
  constructor
  · -- ⊢ x ∈ A ∩ B → x ∈ B ∩ A
    rintro ⟨hA, hB⟩
    -- hA : x ∈ A
    -- hB : x ∈ B
    -- ⊢ x ∈ B ∩ A
    exact ⟨hB, hA⟩
  · -- ⊢ x ∈ B ∩ A → x ∈ A ∩ B
    rintro ⟨hB, hA⟩
    -- hB : x ∈ B
    -- hA : x ∈ A
    -- ⊢ x ∈ A ∩ B
    exact ⟨hA, hB⟩

ext x is the extensionality principle: “let x be an element; let us prove that it is in one side if and only if it is in the other”. rintro is intro plus obtain in a single step.

Exercises.

1. ∃ x : ℝ, x + 3 = 5.
2. (∀ x, P x ∧ Q x) → ∀ x, P x.
3. A ⊆ B → B ⊆ C → A ⊆ C for sets of ℕ.
4. A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C). It is long; do it on paper first.
5. Challenge: (∃ x, ∀ y, R x y) → ∀ y, ∃ x, R x y.

Teaching tips

• Delicate point. The order of the quantifiers. Ask them to read the statement and the goal aloud after each tactic.
• Common mistake. Giving the witness too early or too late: in ∀ ε, ∃ δ, … first intro ε, then use; if the order is reversed, the proof is no longer possible. It is an excellent occasion for them to see why the order matters.
• On Set. Many students expect x ∈ A ∩ B to be opaque. Show them that it is transparent: hx.1 works.
• Double inclusion. It is worth teaching Set.Subset.antisymm as an alternative to ext, but only as a curiosity.

Topic 4. Equality and calculation

Content

Objectives. Rewrite with rw, chain equalities with calc and let Lean do the routine algebra.

4.1 Rewriting. rw [h] replaces in the goal each occurrence of the left-hand side of h by the right-hand side.

example
  (a b c : ℕ)
  (h1 : a = b)
  (h2 : b = c)
  : a = c :=
by
  rw [h1]
  -- ⊢ b = c
  rw [h2]

example
  (a b c : ℕ)
  (h1 : a = b)
  (h2 : b = c)
  : a = c :=
by
  rw [h1, h2]

4.2 Chains of calculations. Lean lets you write the proof the way we would on a blackboard:

example
  (a b : ℝ)
  (h : a = 2 * b)
  (hb : b = 3)
  : a = 6 :=
by
  calc a = 2 * b := h
       _ = 2 * 3 := by rw [hb]
       _ = 6     := by norm_num

Each line is an equality with its justification. The underscore _ means “what was on the previous line”.

4.3 Automatic proofs.

example
  (a b : ℝ)
  : (a + b)^2 = a^2 + 2*a*b + b^2 :=
by
  ring

example
  (a b : ℝ)
  (h : a ≤ b)
  : a + 1 ≤ b + 1 :=
by
  linarith

example
  (a b : ℝ)
  : a * b ≤ (a^2 + b^2) / 2 :=
by
  nlinarith [sq_nonneg (a - b)]

In the last example, sq_nonneg (a - b) is the hint: the fact 0 ≤ (a - b)^2. It is exactly what we would say on paper.

Exercises.

1. (a + b) * (a - b) = a^2 - b^2 in ℝ with ring.
2. Prove 4.2 with rw and norm_num without calc.
3. a ≤ b → c ≤ d → a + c ≤ b + d with linarith.
4. 0 ≤ a^2 + b^2 with positivity.
5. Challenge: 2*a*b ≤ a^2 + b^2 with nlinarith and the right hint.

Teaching tips

• Balance. Many students discover ring and linarith and use them for everything. That is fine: they are arithmetic provers, not cheap shortcuts. What is worth ensuring is that they know how to do the long version with calc when the automatic one fails.
• When linarith fails. When there are products of variables. It is the occasion to introduce nlinarith and hints. Make it explicit that the hint is the mathematical idea.
• Common mistakes.
  • rw rewrites all the occurrences, not just the desired one; if you need to control it, use rw [h] at h2 or nth_rewrite.
  • rw fails with “motive is not type correct” or “did not find instance”; it is almost always a problem of syntactic form, not of mathematics.
  • Alignment of calc.
• Key message. Automation closes obvious steps; the human work lies in choosing the steps.

Topic 5. Induction and recursion

Content

Objectives. Do induction on ℕ, work with finite sums and define recursive functions.

5.1 Induction. The scheme is the one from paper: base case and inductive step.

theorem gauss_sum
  (n : ℕ)
  : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) :=
by
  induction n with
  | zero =>
    -- ⊢ 2 * ∑ i ∈ Finset.range (0 + 1), i = 0 * (0 + 1)
    simp
  | succ k ih =>
    -- k : ℕ
    -- ih : 2 * ∑ i ∈ Finset.range (k + 1), i = k * (k + 1)
    -- ⊢ 2 * ∑ i ∈ Finset.range (k + 1 + 1), i = (k + 1) * (k + 1 + 1)
    rw [Finset.sum_range_succ, mul_add, ih]
    -- ⊢ k * (k + 1) + 2 * (k + 1) = (k + 1) * (k + 1 + 1)
    ring

In succ k ih there appear k (the value for which we already know the result) and ih, the induction hypothesis. Finset.range (n + 1) is {0, 1, …, n} and Finset.sum_range_succ says that summing up to k+1 is summing up to k and adding the last term.

5.2 Recursive definitions.

def fact : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fact n

theorem fact_pos
  (n : ℕ)
  : 0 < fact n :=
by
  induction n with
  | zero =>
    -- ⊢ 0 < fact 0
    simp [fact]
  | succ k ih =>
    -- k : ℕ
    -- ih : 0 < fact k
    -- ⊢ 0 < fact (k + 1)
    show 0 < (k + 1) * fact k
    -- ⊢ 0 < (k + 1) * fact k
    exact Nat.mul_pos (Nat.succ_pos k) ih

#eval fact 5
-- 120

#eval computes: it is the “programming” part, and here it only serves to check that the definition does what is expected (it returns 120).

Exercises.

1. Prove by induction that ∑ i ∈ Finset.range (n + 1), (2 * i + 1) = (n + 1)^2.
2. Define double : ℕ → ℕ by recursion and prove double n = 2 * n.
3. Prove that fact n ≥ 1 without using fact_pos.
4. Challenge: 2^n ≥ n + 1 by induction (hint: omega or nlinarith in the step).

Teaching tips

• Key idea. Lean's induction is literally the induction principle. Stress that ih is the hypothesis that on paper we would write as “suppose it true for k”.
• Summation notation. Students get blocked by Finset. It is enough to say that Finset.range n is {0,…,n−1} and that ∑ i ∈ S, f i is the usual sum. No further explanation is needed.
• Common mistakes.
  • Confusing n and n + 1 in the cases.
  • Expecting simp to close the inductive step, when it usually needs the sum lemma.
  • rw fails because the goal shows k + 1 + 1 and not k + 2.
• Debugging trick. When the inductive step does not work out, ask them to write the goal and the hypothesis on paper and to ask themselves which equality connects them.

Topic 6. Your own definitions

Content

Objectives. Define new mathematical concepts (properties, structures) and prove statements about them.

6.1 Defining a property. Lean does not know what “injective” means in our text until we write it down (Mathlib already has Function.Injective, but defining it yourself is the best way to understand it).

def MyInjective (f : ℕ → ℕ) : Prop :=
  ∀ a b, f a = f b → a = b

example : MyInjective (fun n => n + 1) :=
by
  intro a b h
  -- a b : ℕ
  -- h : (fun n => n + 1) a = (fun n => n + 1) b
  -- ⊢ a = b
  simpa using h

After intro, h says (fun n => n + 1) a = (fun n => n + 1) b; simpa simplifies and concludes.

6.2 Limit of a sequence.

def Converges (a : ℕ → ℝ) (l : ℝ) : Prop :=
  ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, |a n - l| < ε

example
  (c : ℝ)
  : Converges (fun _ => c) c :=
by
  intro ε hε
  -- ε : ℝ
  -- hε : ε > 0
  -- ⊢ ∃ N, ∀ n ≥ N, |(fun x => c) n - c| < ε
  use 0
  -- ⊢ ∀ n ≥ 0, |(fun x => c) n - c| < ε
  intro n hn
  -- n : ℕ
  -- hn : n ≥ 0
  -- ⊢ |(fun x => c) n - c| < ε
  simpa using hε

It is the ε-N definition from Analysis courses, written almost identically. The proof also follows the paper script: given ε, we choose N, and for each n the absolute value is 0 < ε.

6.3 Structures. They are used to group data.

structure Point where
  x : ℝ
  y : ℝ

def Point.norm2 (p : Point) : ℝ :=
  p.x^2 + p.y^2

theorem Point.norm2_nonneg
  (p : Point)
  : 0 ≤ p.norm2 :=
by
  unfold Point.norm2
  -- ⊢ 0 ≤ p.x ^ 2 + p.y ^ 2
  positivity

6.4 Types and universes, only what is essential. ℕ, ℝ, Set ℕ and ℕ → ℝ are types; x : ℕ is read “x is an element of ℕ”. That is enough. Mathlib uses classes (Group, Field, …) for algebraic structures, which will be seen in passing.

Exercises.

1. Define Increasing (a : ℕ → ℝ) and prove that fun n => (n : ℝ) is increasing.
2. Prove Converges a l → Converges a l' → l = l' (the limit is unique). It is a challenge; start by writing the proof on paper with ε/2.
3. Define the structure MyRat with a numerator and a denominator and a function add. (Only the definition; proving properties is optional.)

Teaching tips

• What matters. That the student sees that their mathematical vocabulary is translated literally. Analysis students usually get hooked here.
• Common mistake. A definition that looks correct but is not (for example, forgetting ε > 0). Lean does not warn: the definition compiles. The lesson is that Lean verifies proofs, not that the definitions are the ones we intended.
• Frequent questions. “Why not use Mathlib's definition?” Because learning to define is part of the craft; later it is replaced by Mathlib's, with Filter.Tendsto, and the difference is discussed.
• Types and functions. If doubts about type theory arise, answer with the motto “a type is like a set, except that each element has a single type”.

Topic 7. Finding your way around Mathlib

Content

Objectives. Find lemmas you do not know, read their statements and apply them.

7.1 The real problem. Nobody memorizes Mathlib. The skill trained here is searching.

7.2 Tools.

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

example
  (a b : ℕ)
  (hb : 0 < b)
  (h : a ∣ b)
  : a ≤ b :=
by
  exact?

Lean proposes Nat.le_of_dvd hb h. Good practice is to copy the suggestion instead of leaving exact?.

7.3 Naming conventions. Mathlib's names are descriptive: add_comm, mul_pos, sq_nonneg, Finset.sum_range_succ. With time you learn to guess them: a_lt_b_iff usually means “a < b if and only if…”.

7.4 Working locally. When the student wants to carry on alone: install Lean and VS Code following the official instructions, and create a project with Mathlib (lake new my_project math). For the course it is enough to provide a ready-made template and a written start-up procedure, to prevent anyone from getting stuck on the installation.

Exercises.

1. For each of these statements, find the Mathlib lemma that solves it:
   • 0 < a → 0 < b → 0 < a * b;
   • |a + b| ≤ |a| + |b|;
   • a ≤ b → a ≤ b + c if 0 ≤ c.
2. Use #check to read the statement of Finset.sum_comm and explain in your own words what it says.
3. Challenge: prove Nat.Prime 7 in two ways (norm_num and decide).

Teaching tips

• Pedagogical goal. Demystify. The student should understand that looking for the lemma is a normal part of the work, just like looking up a theorem in a book.
• Installation. If it is done locally, set aside a separate session and keep close company. It is the point where most students get lost. A shared template saves hours.
• Common mistakes.
  • Leaving exact? in the submission: it is slow and not a stable proof.
  • Generic names (add_comm) work for several types; if the student gives a wrong type, Lean complains with long messages. Teach them to read the last line of the error first.
• Good practices. Save often, comment with --, split long proofs into named auxiliary lemmas.

Topic 8. Final project

Content

Objective. Formalize a complete elementary result and present it.

Project options (choose one).

1. Set theory. De Morgan's laws and distributivity for sets and families of sets.
2. Arithmetic. Sum of the first n odd numbers, Gauss's formula, Bernoulli's inequality.
3. Analysis. Uniqueness of the limit and limit of the sum of two convergent sequences, with the ε-N definition from Topic 6.
4. Algebra. In a group, uniqueness of the identity and of the inverse, using Mathlib's Group.
5. Free choice. A proposition from a course the student is taking, agreed with the teacher.

Deliverables. A .lean file without sorry, with comments explaining the strategy, plus a page with the paper proof and a short reflection on what was hardest in Lean.

Teaching tips

• What to assess.
  1. That it compiles.
  2. That the statements are faithful to the mathematical text.
  3. That the structure (auxiliary lemmas) is clear.
  4. That the student can explain their own proof.
• Advice. Require them to first write the paper proof divided into lemmas; the Lean version is the translation. Projects improvised directly in Lean end in frustration.
• Extensions. For advanced groups: basic topology, a little Galois theory, or contributing a small lemma to Mathlib.

Appendix A. Tactics cheat sheet

Appendix B. How to read an error

1. Read first the line marked in red, not the whole message.
2. “unsolved goals” means the proof is not finished: look at which goal remains.
3. “type mismatch” indicates that you have given something that does not fit the goal: compare the two types.
4. “unknown identifier” is usually a spelling mistake or a missing import.
5. If you do not understand the message, put sorry in the step, check that the rest compiles and move on.

Appendix C. Resources

• The Natural Number Game (Kevin Buzzard): a playful entry point to Lean, perfect as an activity before Topic 1.
• Lean Game Server (the same server as the Natural Number Game): includes other games, such as the ones on set theory, logic or the integers. They are a natural continuation of the first one.
• The mechanics of proof (Heather Macbeth): an introduction to Lean for mathematicians.
• Mathematics in Lean (Jeremy Avigad and Patrick Massot): the reference interactive text for mathematicians, ideal as complementary reading.
• Theorem Proving in Lean 4: a more technical text, useful for understanding the type-theory background.
• Matemáticas Lean 4 (José A. Alonso): a book (in Spanish) on elementary mathematics using Lean 4.
• Lean 4 proof challenges (José A. Alonso): a collection of Lean 4 proof exercises with several solutions, from the most automatic to the most detailed, and with links to Lean 4 Web to experiment with the code from the browser. Some exercises also include a video explaining how to build the solutions.
• Calculemus (José A. Alonso): a blog of Lean exercises.
• Glimpse of Lean (Patrick Massot): Lean 4 exercises designed for mathematicians who already know the basics, with a very practical approach.
• Formalising Mathematics (Kevin Buzzard): a repository of notes and exercises for formalizing mathematics in Lean.
• 100 Theorems in Lean: an archive of classical formalized theorems, which gives a realistic idea of how hard formalization is.
• Mathlib documentation and the Lean Zulip forum: resources for asking questions and looking up definitions and results.
• Learning Lean on the community's official page: the general index of resources.

Appendix D. Suggested schedules

• Short course (4 sessions). Topics 1, 2, 3 and 4, with a mini-project on sets.
• Standard course (8 sessions). One topic per session, with the final project as the work of the last week.
• Intensive course (2 days). Morning: Topics 1 to 3. Afternoon: Topics 4 and 5. Second day: Topics 6 and 7, and a mini-project in groups.