Each worksheet prints cleanly on A4 or Letter. Answer keys are on a separate page.

The Lumenary · Early undergraduate

Formalising mathematics in Lean and Mathlib

Name: ______________________

Date: ______________________

You will learn to

Formalise definitions and proofs about sets, functions and quantifiers in Lean, such as the facts that a composite of injections is injective and that images preserve unions
Use structures, type classes and Mathlib's algebraic hierarchy to state and prove results about every monoid or group at once
Search Mathlib for existing results, and explain the trade-off between citing a library lemma and proving a result from scratch
Recognise the conventions and hidden hypotheses that formalisation exposes, such as $x/0 = 0$ and truncated subtraction on $\N$
Explain what a machine check guarantees — and what it does not — using the kernel, #print axioms, and the need for definitions to match standard usage

1.
With f : α → β and g : β → γ, which Lean statement says that a composite of injective functions is injective?
- A.Injective g → Injective f → Injective (g ∘ f)
- B.Injective (g ∘ f) → Injective g
- C.∃ f g, Injective (g ∘ f)
- D.Injective g ∧ Injective f
2.
To prove that $g \circ f$ is injective, we assume $g(f(x)) = g(f(y))$ and must show $x = y$ . Which fact do we use first?
- A.Injectivity of $g$ , to get $f(x) = f(y)$
- B.Injectivity of $f$ , to get $x = y$ directly
- C.Surjectivity of $g$
- D.Associativity of composition
3.
Which function $f : \N \to \N$ gives sets $S, T$ with $f(S \cap T) \ne f(S) \cap f(T)$ ?
- A. $f(n) = 0$ for all $n$
- B. $f(n) = n + 1$
- C. $f(n) = 2n$
- D. $f(n) = n$
4.
Which of these statements about natural numbers are true? (Choose all that apply.)
- A. $\forall n\ \exists m\ \ n < m$
- B. $\exists m\ \forall n\ \ n < m$
- C. $\exists m\ \forall n\ \ m \le n$
- D. $\forall n\ \exists m\ \ m < n$
5.
In Lean, with natural numbers, what is the value of (5 : ℕ) - 8 + 8?
6.
In Mathlib, (7 : ℝ) / 0 = 0 is a theorem (div_zero). What follows?
- A.Nothing false: laws such as a / b * b = a require the hypothesis b ≠ 0, so the convention cannot be used to cancel a zero.
- B.7 = 0, by multiplying both sides by 0.
- C.Lean's logic is inconsistent.
- D.Real analysis defines division by zero.
7.
#print axioms limit_unique reports [propext, Classical.choice, Quot.sound]. What does this tell you?
- A.The proof is complete (no sorry) and uses only Lean's three standard axioms, including choice.
- B.The proof is incomplete, because it depends on axioms.
- C.The proof is constructive.
- D.limit_unique was itself assumed as an axiom.
8.
In the proof that a group in which every $x$ satisfies $x^2 = 1$ is commutative, we write $ab = (ab)^{-1} = b^{-1}a^{-1} = ba$ . Which group law justifies the middle equality?
- A.The inverse of a product is the product of the inverses in reverse order (Mathlib's mul_inv_rev).
- B.Commutativity of multiplication.
- C. $x^{-1} = x$ for all $x$ .
- D.Uniqueness of the identity element.
9.
Write find_counterexample(a, b) that searches all functions $f$ from $\{0, \dots, a-1\}$ to $\{0, \dots, b-1\}$ (as tuples of values) and all pairs of subsets $S, T$ of the domain, and returns the first (f, S, T) with $f(S \cap T) \ne f(S) \cap f(T)$ (with S, T as Python sets), or None if there is none. Use itertools.
Computational — Practice

Answer key — Formalising mathematics in Lean and Mathlib

1.
Option (a). Informal "if $g$ and $f$ are injective then $g \circ f$ is injective" becomes Injective g → Injective f → Injective (g ∘ f) (curried implications). The lesson proves it both from scratch (injective_comp) and by citing Mathlib (hg.comp hf).
2.
From $g(f(x)) = g(f(y))$ , injectivity of $g$ gives $f(x) = f(y)$ , and then injectivity of $f$ gives $x = y$ . In the Lean proof, apply hf comes first because apply works backwards from the goal — the reasoning order and the text order are mirror images.
3.
Equality can only fail for a non-injective $f$ , and among the options only the constant function is not injective. With $S = \{0\}$ and $T = \{1\}$ : $S \cap T = \varnothing$ , so $f(S \cap T) = \varnothing$ , while $f(S) = f(T) = \{0\}$ . This is the Lean theorem image_inter_ne; the first experiment confirms on all small examples that equality for all $S, T$ holds exactly for injective $f$ .
4.
True: (a) with $m = n + 1$ , and (c) with $m = 0$ . False: (b), since $n = m$ fails; (d), since $n = 0$ has nothing below it. (a) and (b) differ only in the order of the quantifiers — the Lean theorem forall_exists_not_imp shows that $\forall\exists$ does not imply $\exists\forall$ .
5.
On ℕ, 5 - 8 = 0 (truncated subtraction), so 5 - 8 + 8 = 8, not 5. The law a - b + b = a holds only when b ≤ a (Nat.sub_add_cancel). Formal statements carry such hypotheses explicitly; informal ones often leave them implicit.
6.
Option (a). Lean functions are total, so x / 0 must denote something; Mathlib chooses 0. To derive anything about real division you need laws like div_mul_cancel₀ : b ≠ 0 → a / b * b = a, and these carry the hypothesis b ≠ 0. So from 7 / 0 = 0 nothing false follows; the lesson's theorem div_mul_cancel_needs_hyp shows that the cancellation law without its hypothesis is false.
7.
#print axioms lists the axioms a proof depends on. Here they are the three standard ones: propositional extensionality, quotient soundness and choice. There is no sorryAx, so the proof is complete. Compare injective_comp, which depends on no axioms at all: it is pure logic plus the definition of composition.
8.
The middle step $(ab)^{-1} = b^{-1}a^{-1}$ holds in every group: $(ab)(b^{-1}a^{-1}) = 1$ and inverses are unique (the lesson's inv_unique). The outer steps use the hypothesis via $x^{-1} = x$ . In Lean the step is mul_inv_rev a b, which is why comm_of_sq_eq_one works for every Mathlib Group.

import itertools

def find_counterexample(a, b):
    subsets = [set(c) for k in range(a + 1)
               for c in itertools.combinations(range(a), k)]
    for f in itertools.product(range(b), repeat=a):
        image = lambda s: {f[x] for x in s}
        for S in subsets:
            for T in subsets:
                if image(S & T) != image(S) & image(T):
                    return f, S, T
    return None

For $a = 2$ , $b = 1$ it finds the constant function with $S = \{0\}$ , $T = \{1\}$ . For $a = 1$ every function is injective, so no counterexample exists — consistent with Mathlib's Set.image_inter. A finite search can refute a general claim but not prove one; the theorem for injective functions is proved in the lesson.