Skip to content
The Lumenary
Early undergraduateComputationLesson available

Formalising mathematics in Lean and Mathlib

Formalising undergraduate mathematics in Lean 4 with Mathlib: structures and type classes, sets and functions, quantifier reasoning, algebraic structures, and searching and contributing to a large library.

math.comp.formal-proof-lean

Open lesson Show everything needed to reach this topic

Builds on

First steps in Lean

Required prerequisites, all the way down: 16

You will learn to

  • Formalise definitions and proofs about sets, functions and quantifiers, such as the fact that a composite of injections is injective.
  • Use Mathlib's algebraic hierarchy to state and prove results about groups and rings.
  • Search Mathlib for existing results and explain the trade-off between using library lemmas and proving from scratch.

Definition

  • Mathlib is the community-maintained mathematical library for Lean 4.
  • A type class packages structure, such as a group operation, which Lean then finds automatically by instance search.
  • A structure in Lean is a type whose elements bundle several fields, such as the carrier operations and laws of a monoid.

Theorem

  • Mathlib's Function.Injective.comp states that a composite of injective functions is injective.
  • Lean's #print axioms command lists the axioms on which a proof depends.
  • A formal library is useful only if its definitions match standard mathematical usage, which people must check.

Common misconceptions

  • Thinking formalisation is mere translation; it often exposes hidden assumptions and edge cases.
  • Believing Lean's convention x / 0 = 0 changes mathematics; it is a definitional convenience, and theorems carry hypotheses such as x ≠ 0 where needed.

Leads to

Formalising published mathematics

Optional discoveries

Learning pathways

Further reading