The language of mathematics

A reading aid for non-specialists: what symbols such as ∀, ∣, ⇔ and Σ mean, how a mathematical paper is structured, and how to read a proof in Lean line by line.

The chapters of this section write their theorems and proofs the way mathematical papers do. It looks strange at first, but it is only a shorthand. This chapter explains it. There is no need to learn it by heart, you can look things up here whenever a symbol turns up.

Why a script of its own?

The same theorem, once in words:

For every natural number n, the sum of all numbers from 1 to n equals the product of n and n plus one, divided by two.

And once in the notation of mathematics:

\forall n \in \mathbb{N}: \quad \sum_{i=1}^{n} i = \frac{n(n+1)}{2}

Both say exactly the same. The second version is shorter, you take it in at a glance, and it leaves no room for misunderstanding. That is why mathematicians invented these symbols over the centuries. The line is read: “For all n in the natural numbers: the sum of i from i equals 1 to n is n times n plus 1, over 2.”

Numbers and sets

Symbol	read as	Example
$\mathbb{N}$	the natural numbers 1, 2, 3 …	$10 \in \mathbb{N}$
$\mathbb{N}_0$	the natural numbers with zero	$0 \in \mathbb{N}_0$
$\in$	is an element of, belongs to	$7 \in \mathbb{N}$
$\notin$	does not belong to	$\tfrac{1}{2} \notin \mathbb{N}$
$\{\, \dots \,\}$	the set of …	$\{1, 2, 5, 10\}$
$\{x : \dots\}$	the set of all x for which … holds	$\{d \in \mathbb{N} : d \mid 10\} = \{1,2,5,10\}$

Calculating and dividing

Symbol	read as	Example
$a \cdot b$ , $ab$	a times b	$4 \cdot 5 = 20$
$\frac{a}{b}$	a divided by b	$\frac{20}{2} = 10$
$\sum_{i=1}^{n} i$	sum of i from 1 to `n`	$\sum_{i=1}^{4} i = 1+2+3+4$
$\prod_{i=1}^{n} i$ , $n!$	product of i from 1 to `n`, “`n` factorial”	$4! = 1 \cdot 2 \cdot 3 \cdot 4 = 24$
$a \mid b$	a divides b	$5 \mid 10$
$a \nmid b$	a does not divide b	$4 \nmid 10$
$\gcd(a, b)$	greatest common divisor	$\gcd(10, 4) = 2$
$a \equiv b \pmod{m}$	a and b leave the same remainder on division by m	$25 \equiv 1 \pmod{6}$
$\lfloor x \rfloor$	x rounded down	$\lfloor 2.5 \rfloor = 2$

A word on the vertical bar: $a \mid b$ is a statement (“5 divides 10”, which is true or false), not a calculation. $\frac{b}{a}$ , by contrast, is a number. The symbol is an upright bar, not a fraction bar, precisely so that the two are not confused.

Logic

Symbol	read as	Example
$\forall$	for all	$\forall n \in \mathbb{N}: n + 1 > n$
$\exists$	there is	$\exists d: 1 < d < 10 \text{ and } d \mid 10$
$\land$ , $\lor$	and, or	$2 \mid 10 \land 5 \mid 10$
$\lnot$	not	$\lnot\, (3 \mid 10)$
$A \Rightarrow B$	A implies B, if A then B	$4 \mid n \Rightarrow 2 \mid n$
$A \Leftrightarrow B$	A if and only if B	$2 \mid n \Leftrightarrow n \text{ even}$
$:=$	is defined as	$T(n) := \sum_{i=1}^n i$

The “or” of mathematics is always inclusive: $A \lor B$ is also true when both hold. And $A \Rightarrow B$ says nothing about what happens when A is false. From “If it rains, the street is wet” it does not follow that the street is dry when it does not rain.

How a paper is structured

Mathematical texts consist of a few building blocks that always have the same names:

Definition: a term is fixed. From then on the word means exactly that and nothing else.
Theorem: an important proven statement.
Lemma: a helper theorem, needed mainly to prove another theorem.
Corollary: a theorem that follows from an earlier one in a few lines.
Proof: the justification. Its end is marked by the sign ∎ or the abbreviation q.e.d., Latin quod erat demonstrandum, “which was to be shown”.

Within a proof, too, there are fixed phrases:

“Let n ∈ ℕ” means: we take some natural number without saying which. Whatever follows holds for every one.
“Without loss of generality”: we consider only one case, because the others go the same way.
“Suppose …” often opens a proof by contradiction: you assume the opposite and show that nonsense follows.
Base case and inductive step are the two parts of a proof by induction, the first domino and each next one (see What is a proof?).

A small complete example in this form:

Theorem

For all $n \in \mathbb{N}$ , $n(n+1)$ is even.

Proof

Let $n \in \mathbb{N}$ . Of the two consecutive numbers $n$ and $n+1$ exactly one is even. A product with an even factor is even. Hence $2 \mid n(n+1)$ .

∎

Read line by line: the theorem claims something about all natural numbers. “Let n ∈ ℕ” picks out an arbitrary one. The next two sentences are the justification, the last writes the result in symbols, and ∎ says: done. All proofs in this section are built exactly this way.

How to read Lean

Below important theorems there is a box that unfolds to show the same proof in Lean, a programming language for proofs developed since 2013. Lean is stricter than any human reader: it accepts a proof only if every step follows from the rules of logic. Here is the proof about triangular numbers from Chapter 1, explained piece by piece.

/-- The n-th triangular number 1 + 2 + … + n -/

A comment. Text between /-- and -/ is written for people, Lean skips it. One-line comments begin with --.

def triangle : Nat → Nat
| 0 => 0
| n + 1 => triangle n + (n + 1)

A definition. def introduces a new name, here triangle. After the colon comes what kind of thing it is: Nat → Nat means “a rule that turns a natural number into a natural number”. In Lean Nat are the natural numbers with zero, that is $\mathbb{N}_0$ . The two lines with | say how to calculate: the zeroth triangular number is 0, and the triangular number of n + 1 is that of n plus n + 1. In the notation of papers: $T(0) := 0$ and $T(n+1) := T(n) + (n+1)$ .

example : triangle 4 = 10 := rfl

An example without a name. Before := stands the claim, after it the proof. rfl stands for reflexivity: after calculating, both sides are simply equal. Lean works out $T(4) = 10$ .

theorem two_triangles (n : Nat) :
  2 * triangle n = n * (n + 1) := by

A theorem. theorem announces it, then comes its name. (n : Nat) means “Let n be a natural number”. After the colon stands the claim $2 \cdot T(n) = n(n+1)$ , with * as the multiplication sign. := by opens the proof, as a sequence of commands that Lean carries out one after another.

induction n with
| zero => rfl

induction n says: proof by induction on n. Lean then demands two parts. zero is the base case, n = 0. There $2 \cdot 0 = 0 \cdot 1$ , and rfl suffices.

| succ n ih =>
  rw [triangle, Nat.mul_add, ih]
  grind

succ is the inductive step from n to n + 1 (successor). ih is the name for the induction hypothesis, that is, that the formula already holds for n. rw (rewrite) replaces expressions: first triangle (n + 1) by its definition, then the product is multiplied out (Nat.mul_add is the distributive law $a(b+c) = ab + ac$ ), then the induction hypothesis is inserted. What remains is $n(n+1) + 2(n+1) = (n+1)(n+2)$ , a calculation with brackets that grind settles by itself.

The most important words and symbols of Lean at a glance:

Lean	means	in papers
`Nat`	natural numbers with 0	$\mathbb{N}_0$
`Prop`	a statement that can be true or false
`n : Nat`	`n` is a natural number	$n \in \mathbb{N}_0$
`∀ k, …`	for all `k` … holds	$\forall k$
`A → B`	A implies B	$A \Rightarrow B$
`A ↔ B`	A if and only if B	$A \Leftrightarrow B$
`∧`, `∨`	and, or	$\land, \lor$
`d ∣ n`	d divides `n`	$d \mid n$
`Nat.gcd n k`	greatest common divisor	$\gcd(n,k)$
`n / 2`	division rounding down	$\lfloor n/2 \rfloor$
`intro h`	“Suppose h” or “Let …”
`exact h`	this is exactly h
`omega`	solves equations and inequalities with + and numbers by itself
`decide`	works through finitely many cases completely
`·`	start of a case in a case distinction

That is all you need to follow the course of a Lean proof. If you want to change one, open it in the browser through the link in the box. Lean will then tell you at once whether the proof still holds.

Where the symbols come from

Most of the symbols are younger than one might think. Plus and minus first appear in print in 1489 in Johannes Widmann’s book in Leipzig. The equals sign was invented in 1557 by the Welshman Robert Recorde, “bicause noe .2. thynges, can be moare equalle” than two parallel strokes. Leonhard Euler introduced the summation sign Σ in 1755. The sign ∈ for “is an element of” comes from Giuseppe Peano in 1889, the ∃ for “there is” also from him in 1897, the ∀ for “for all” from Gerhard Gentzen in 1935. The black box ∎ at the end of a proof was made customary by the mathematician Paul Halmos in the middle of the twentieth century. The Pythagoreans knew none of these signs. They wrote everything in words or laid it out with pebbles.

Sources and further reading

Sources

Robert Recorde, The Whetstone of Witte, London 1557 (the equals sign)
Leonhard Euler, Institutiones calculi differentialis, St Petersburg 1755 (the summation sign)
Giuseppe Peano, Arithmetices principia, nova methodo exposita, Turin 1889
Gerhard Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift 39, 1935 (the sign ∀)
Leonardo de Moura et al., The Lean Theorem Prover, Automated Deduction, CADE-25, LNCS 9195, Cham 2015