Factors, multiples and primes

Lens

MotivationH

Chairs for the assembly

Mr Mensah's class in Accra is setting out 24 chairs for an assembly. He wants equal rows with no chair left over. They could make $2$ rows of $12$ , or $3$ rows of $8$ , or $4$ rows of $6$ , or even one long row of $24$ .

The next week there are 23 chairs. Now nothing works except one long line of $23$ , or $23$ rows of one chair each!

Why can $24$ be arranged in so many ways and $23$ in only one? The answer leads to some of the oldest and deepest ideas in mathematics: factors, multiples and prime numbers.

IntuitionH

Rectangles of dots

Every way of arranging chairs in equal rows is a rectangle of dots, just like the arrays in whole-number arithmetic. A rectangle with $4$ rows of $6$ shows that $24 = 4 \times 6$ . Try different row lengths for $24$ below, and then try $23$ :

How many rectangles can you make?

Arrange dots in equal rows. When nothing is left over, you have found a factor pair.

Number of dots24Dots in each row12

24 = 2 × 12

24 dots make 2 full rows of 12, with nothing left over: 12 and 2 are factors of 24.

Every rectangle you can make with 24 dots (tap one):

24 has 8 factors: 1, 2, 3, 4, 6, 8, 12, 24

24 is composite: it can be arranged in more than one rectangle.

For $24$ you find the rectangles $1 \times 24$ , $2 \times 12$ , $3 \times 8$ and $4 \times 6$ (and the same ones turned round). For $23$ the only rectangle is a single line. Numbers bigger than $1$ that, like $23$ , can only make a line are the primes.

DefinitionsH

The words we need

Definition— factor and multiple

If $a = b \times k$ for some whole number $k$ , we say $b$ is a factor of $a$ , and $a$ is a multiple of $b$ . For example, $12 = 3 \times 4$ , so $3$ is a factor of $12$ and $12$ is a multiple of $3$ .

The two words point in opposite directions. The factor fits exactly into the multiple; the multiple is built from copies of the factor. We also say that $a$ is divisible by $b$ , or that $b$ divides $a$ .

Definition— prime and composite

A prime number is a whole number greater than $1$ whose only factors are $1$ and itself. A composite number is a whole number greater than $1$ that is not prime.

The number $1$ is neither prime nor composite. It is not greater than $1$ , and it has only one factor.

Definition— common factors and common multiples

A common factor of two numbers is a factor of both. The biggest one is their greatest common factor. A common multiple is a multiple of both, and the smallest one above $0$ is their least common multiple.

Worked examplesH

Worked examples

Example— The factors of 36, in pairs

Look for factors in pairs, starting from $1$ :

36 = 1 \times 36 = 2 \times 18 = 3 \times 12 = 4 \times 9 = 6 \times 6.

$5$ is not a factor, because $36 = 7 \times 5 + 1$ . After $6 \times 6$ the pairs only repeat the other way round ( $9 \times 4$ , $12 \times 3$ , …), so we can stop. The factors of $36$ are $1, 2, 3, 4, 6, 9, 12, 18, 36$ : nine of them. The number is odd because $6$ pairs up with itself.

Example— Common factors and common multiples

Factors of $24$ : $1, 2, 3, 4, 6, 8, 12, 24$ . Factors of $36$ : $1, 2, 3, 4, 6, 9, 12, 18, 36$ . The common factors are $1, 2, 3, 4, 6, 12$ , and the greatest common factor is $12$ .
Multiples of $4$ : $4, 8, 12, 16, 20, 24, \dots$ Multiples of $6$ : $6, 12, 18, 24, \dots$ The common multiples are $12, 24, 36, \dots$ , and the least common multiple is $12$ , not $4 \times 6 = 24$ .

Example— Prime or not?

$2$ is prime. It is the only even prime, because every other even number has the factor $2$ .
$9$ is odd but not prime: $9 = 3 \times 3$ .
$51 = 3 \times 17$ and $91 = 7 \times 13$ are composite. They fool many people!
$97$ is prime. To be sure, we only need to try the primes $2, 3, 5, 7$ (see the proofs below for why we can stop there).

Example— A factor tree

To write $360$ as a product of primes, split it into any two factors, and keep splitting until every branch ends in a prime. Two people may grow different trees, but they reach the same primes:

Two different factor trees for 360. The left tree starts with 36 × 10, the right with 8 × 45. Both end with the same primes (circled): 360 = 2 × 2 × 2 × 3 × 3 × 5.

So $360 = 2 \times 2 \times 2 \times 3 \times 3 \times 5$ . Grown-ups often write this as $2^3 \times 3^2 \times 5$ .

Example— Zero and one

$1$ is a factor of every number, because $a = 1 \times a$ . And $0$ is a multiple of every number, because $0 = b \times 0$ .

Explore

Explore: multiples and the sieve

When do two patterns meet? The grid marks the multiples of $4$ with circles and the multiples of $6$ with squares. The numbers with both marks are the common multiples. Change the numbers and the number of columns.

Multiples on a hundred grid

Mark the multiples of a number and look for patterns. Add a second number to find common multiples.

Multiples of4

and multiples of6

multiple of 4
multiple of 6
common multiple (both)

There are 25 multiples of 4 from 1 to 100.

Common multiples of 4 and 6: 12, 24, 36, 48, 60, 72, 84, 96. The smallest one, 12, is the least common multiple.

Tap a number to see how it is related.

The sieve of Eratosthenes. Cross out $1$ . Then circle $2$ and cross out its other multiples. Circle the next number left, $3$ , and cross out its multiples, and so on. The numbers that survive are the primes. Step through it and notice when the sieve has nothing left to do.

The Sieve of Eratosthenes

Cross out the multiples of each prime in turn. The numbers that are never crossed out are the primes.

prime
crossed out

Step 1 of 7

Here are the numbers from 1 to 100. Press “Next step” to start sieving.

ProofH

Why it all works

Finding factors: when to stop

Factors come in pairs $b \times k$ . As the first number of the pair grows, the second shrinks. Once the first number passes the second, every pair we find is an old pair turned round. So we can stop when the two numbers meet, in the middle, at the side of a square. For $36$ that is $6 \times 6$ . For $24$ we stop after $4 \times 6$ , because $5$ is not a factor and $6 \times 4$ is old.

The smallest factor is always prime

Theorem— smallest factor

For any whole number $n$ greater than $1$ , the smallest factor of $n$ that is bigger than $1$ is a prime.

Proof

Call this smallest factor $p$ . If $p$ were not prime, it would have a factor $q$ with $1 < q < p$ . But a factor of a factor of $n$ is also a factor of $n$ : if $n = p \times k$ and $p = q \times j$ , then $n = q \times (j \times k)$ . So $q$ would be a factor of $n$ smaller than $p$ , which is impossible. So $p$ is prime.

∎

Every number is built from primes

Theorem— factor trees

Every whole number greater than $1$ is either a prime or a product of primes.

Proof

Grow a factor tree. If the number is prime, stop. If not, split it into two factors, each smaller than the number itself, and do the same with each factor. Every split makes the numbers smaller, and whole numbers cannot get smaller for ever. So the tree must stop growing, and it can only stop at primes. The number is the product of those primes.

∎

There is more: the primes at the bottom of the tree are always the same, however you grow it (only their order may change). This is called the fundamental theorem of arithmetic. It is true, but it is harder to prove than it looks. You will meet the proof later, in divisibility and unique factorisation.

For grown-ups · why uniqueness needs a proof

Imagine a world where only even numbers exist. Call an even number an even-prime if it cannot be written as a product of two even numbers. Then $2$ , $6$ , $10$ and $30$ are all even-primes ( $6 = 2 \times 3$ , but $3$ does not exist in this world). And

60 = 6 \times 10 = 2 \times 30

has two different factorisations into even-primes! So uniqueness is a special property of the whole numbers, not something that comes for free. The same thing happens in more serious number systems: among the numbers $a + b\sqrt{-5}$ (with $a$ and $b$ integers), $6 = 2 \times 3 = (1 + \sqrt{-5})(1 - \sqrt{-5})$ , and none of these four factors can be split further. This puzzle helped start the branch of mathematics called algebraic number theory.

The divisibility tests

They all rest on one fact: if a number divides two numbers, it divides their sum. If $a = d \times j$ and $b = d \times k$ , then $a + b = d \times (j + k)$ by the distributive law. In the same way, it divides their difference.

Tests for $2$ , $5$ and $10$ : look at the last digit. Any number is "some tens plus its last digit". For example, $3475 = 347 \times 10 + 5$ . The tens part, $347 \times 10$ , is always a multiple of $10$ , and so also of $2$ and of $5$ . So whether the whole number is divisible by $2$ , $5$ or $10$ depends only on the last digit. $3475$ ends in $5$ , so it is divisible by $5$ but not by $2$ or $10$ .

Tests for $9$ and $3$ : add the digits. The trick is that $10 = 9 + 1$ , $100 = 99 + 1$ , $1000 = 999 + 1$ , and so on. So

572 = 5 \times 100 + 7 \times 10 + 2 = \underbrace{5 \times 99 + 7 \times 9}_{\text{a multiple of } 9} + (5 + 7 + 2).

A number is therefore "a multiple of $9$ , plus its digit sum". So the number and its digit sum leave the same remainder when divided by $9$ , and the number is divisible by $9$ exactly when its digit sum is. Since $9 = 3 \times 3$ , a multiple of $9$ is also a multiple of $3$ , and the same test works for $3$ . For $572$ , the digit sum is $14$ , which is not divisible by $3$ or $9$ , so neither is $572$ .

Why the sieve can stop early

To find the primes up to $100$ , we only need to cross out the multiples of $2$ , $3$ , $5$ and $7$ . Any composite number up to $100$ is a product $a \times b$ of two numbers bigger than $1$ . They cannot both be bigger than $10$ , because then $a \times b$ would be bigger than $10 \times 10 = 100$ . So one of them is at most $10$ , and its smallest prime factor ( $2$ , $3$ , $5$ or $7$ ) has already crossed the number out.

The primes never run out

Theorem— Euclid's theorem

There are infinitely many primes: however far you go, there is always a bigger prime.

Proof

Suppose someone hands you a list of primes, say $2, 3, 5$ . Multiply them all and add $1$ : $2 \times 3 \times 5 + 1 = 31$ . This new number leaves remainder $1$ when divided by each prime on the list, so none of them is a factor. But the new number does have a prime factor (its smallest factor bigger than $1$ ). That prime is not on the list. So no list of primes can ever be complete.

∎

The new number need not be prime itself: $2 \times 3 \times 5 \times 7 \times 11 \times 13 + 1 = 30031 = 59 \times 509$ . But its prime factors, $59$ and $509$ , are new.

Formal mathematicsF

Gideon's precise statements

" $3$ is a factor of $12$ ." — True: $12 = 3 \times 4$ . But " $12$ is a factor of $3$ " is false.
" $1$ is a prime number." — False. The definition needs a number greater than $1$ .
"Every odd number greater than $1$ is prime." — False. $9 = 3 \times 3$ . One counterexample is enough.
" $91$ is prime." — False. $91 = 7 \times 13$ .
"There is a prime bigger than one million." — True. Euclid's proof works for any list of primes.

For grown-ups · the same ideas in Lean, a proof checker

Lean writes " $b$ is a factor of $a$ " as b ∣ a (a tall bar, not the letter l). By definition it means $a = b \times k$ for some $k$ :

factor_defLean 4Proved here from basic factsFormally verified

/-- "`b` is a factor of `a`" (equivalently, "`a` is a multiple of `b`") means `a = b × k`
for some whole number `k`. In Lean this is exactly what `b ∣ a` means, so `Iff.rfl` proves it. -/
theorem factor_def (b a : Nat) : b ∣ a ↔ ∃ k, a = b * k := Iff.rfl

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

three_and_twelveLean 4Proved here from basic factsFormally verified

/-- `3` is a factor of `12` (`12 = 3 × 4`), but `12` is not a factor of `3`: the two words
point in opposite directions. -/
theorem three_and_twelve : 3 ∣ 12 ∧ ¬ (12 ∣ 3) := by decide

Axioms used: propextformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

factors_examplesLean 4Proved here from basic factsFormally verified

/-- The factors of `24` and `36`, as in the lesson. `36` has an odd number of factors because
it is a square: the pair `6 × 6` contributes only one factor. -/
theorem factors_examples :
    factors 24 = [1, 2, 3, 4, 6, 8, 12, 24] ∧ factors 36 = [1, 2, 3, 4, 6, 9, 12, 18, 36] := by
  decide

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

common_factors_24_36Lean 4Proved here from basic factsFormally verified

/-- The common factors of `24` and `36` are `1, 2, 3, 4, 6, 12`, so the greatest common factor
is `12`. -/
theorem common_factors_24_36 : (factors 24).filter (fun d => 36 % d == 0) = [1, 2, 3, 4, 6, 12] := by
  decide

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

lcm_4_6Lean 4Proved here from basic factsFormally verified

/-- `12` is a common multiple of `4` and `6`, and no smaller positive number is.
So the least common multiple of `4` and `6` is `12`, not `4 × 6 = 24`. -/
theorem lcm_4_6 : 4 ∣ 12 ∧ 6 ∣ 12 ∧ ∀ m, m < 12 → 0 < m → ¬ (4 ∣ m ∧ 6 ∣ m) := by decide

Axioms used: propextformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

Primes. Our definition, and a theorem that lets the computer test a number by trying only the numbers below it:

IsPrimeLean 4Formally verified

/-- A **prime** is a whole number greater than `1` whose only factors are `1` and itself. -/
def IsPrime (p : Nat) : Prop := 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

isPrime_iff_boundedLean 4Proved here from basic factsFormally verified

/-- To test whether `p` is prime it is enough to try the numbers smaller than `p`: `p ≥ 2` is
prime exactly when the only factor below `p` is `1`. (A factor of `p` is never bigger than `p`,
by `Nat.le_of_dvd`.) -/
theorem isPrime_iff_bounded (p : Nat) :
    IsPrime p ↔ 2 ≤ p ∧ ∀ m, m < p → m ∣ p → m = 1 := by
  constructor
  · intro ⟨h2, h⟩
    refine ⟨h2, fun m hm hdvd => ?_⟩
    rcases h m hdvd with h1 | hp
    · exact h1
    · omega
  · intro ⟨h2, h⟩
    refine ⟨h2, fun m hdvd => ?_⟩
    have hle : m ≤ p := Nat.le_of_dvd (by omega) hdvd
    by_cases hmp : m = p
    · exact Or.inr hmp
    · exact Or.inl (h m (by omega) hdvd)

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

one_not_primeLean 4Proved here from basic factsFormally verified

/-- `1` is not prime: the definition asks for a number greater than `1`. -/
theorem one_not_prime : ¬ IsPrime 1 := by
  intro ⟨h2, _⟩
  -- `h2 : 2 ≤ 1`, which is false.
  exact absurd h2 (by decide)

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

primes_below_30Lean 4Proved here from basic factsFormally verified

/-- The primes below `30`, found by testing every number. -/
theorem primes_below_30 :
    (List.range 30).filter (fun n => decide (IsPrime n)) = [2, 3, 5, 7, 11, 13, 17, 19, 23, 29] := by
  decide

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

prime_97Lean 4Proved here from basic factsFormally verified

/-- `97` is prime, and `91 = 7 × 13` and `51 = 3 × 17` are not. -/
theorem prime_97 : IsPrime 97 ∧ ¬ IsPrime 91 ∧ ¬ IsPrime 51 := by decide

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

odd_not_always_primeLean 4Proved here from basic factsFormally verified

/-- "Every odd number greater than `1` is prime" is false: `9 = 3 × 3` is a counterexample. -/
theorem odd_not_always_prime : ¬ ∀ n, n % 2 = 1 → 1 < n → IsPrime n := by
  intro h
  have h9 : IsPrime 9 := h 9 (by decide) (by decide)
  exact absurd h9 (by decide)

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

Divisibility tests. First the key fact about sums. Then the last-digit test, proved for $2$ , $5$ and $10$ at once, since all three are factors of $10$ . Then the digit-sum test for $9$ , proved for numbers with any number of digits by induction, one digit at a time:

dvd_add_of_dvdLean 4Proved here from basic factsFormally verified

/-- If `d` is a factor of `a` and of `b`, it is a factor of `a + b`:
from `a = d × j` and `b = d × k`, the distributive law gives `a + b = d × (j + k)`. -/
theorem dvd_add_of_dvd {d a b : Nat} (ha : d ∣ a) (hb : d ∣ b) : d ∣ a + b := by
  obtain ⟨j, hj⟩ := ha
  obtain ⟨k, hk⟩ := hb
  exact ⟨j + k, by rw [hj, hk, Nat.mul_add]⟩

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

last_digit_testLean 4Proved here from basic factsFormally verified

/-- The tests for `2`, `5` and `10`: if `d` is a factor of `10`, then `d` divides `n` exactly
when it divides the last digit `n % 10`. Reason: `n = 10 × (n / 10) + n % 10`, and the first
part is always a multiple of `d`. (`Nat.dvd_add_right`: if `d ∣ x` then `d ∣ x + y ↔ d ∣ y`.) -/
theorem last_digit_test (n d : Nat) (hd : d ∣ 10) : d ∣ n ↔ d ∣ n % 10 := by
  have hsplit : n = 10 * (n / 10) + n % 10 := (Nat.div_add_mod n 10).symm
  have htens : d ∣ 10 * (n / 10) := Nat.dvd_trans hd ⟨n / 10, rfl⟩
  constructor
  · intro h
    rw [hsplit] at h
    exact (Nat.dvd_add_right htens).mp h
  · intro h
    rw [hsplit]
    exact (Nat.dvd_add_right htens).mpr h

Axioms used: propextformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

nine_ruleLean 4Proved here from basic factsFormally verified

/-- A number and the sum of its digits leave the **same remainder** on division by `9`.
Induction on the digits: `d + 10 × m` and `d + s` have the same remainder whenever `m` and
`s` do, because `10 × m = 9 × m + m`. (`omega` does this remainder bookkeeping.) -/
theorem nine_rule (ds : List Nat) : ofDigits ds % 9 = digitSum ds % 9 := by
  induction ds with
  | nil => rfl
  | cons d ds ih =>
    simp only [ofDigits, digitSum]
    omega

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

nine_dvd_iffLean 4Proved here from basic factsFormally verified

/-- The divisibility test for `9`: a number is divisible by `9` exactly when its digit sum is. -/
theorem nine_dvd_iff (ds : List Nat) : 9 ∣ ofDigits ds ↔ 9 ∣ digitSum ds := by
  rw [Nat.dvd_iff_mod_eq_zero, Nat.dvd_iff_mod_eq_zero, nine_rule]

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

example_572Lean 4Proved here from basic factsFormally verified

/-- `572` has digit sum `14`. Both leave remainder `5` on division by `9`, and remainder `2` on
division by `3`, so `572` is divisible by neither. -/
theorem example_572 :
    ofDigits [2, 7, 5] = 572 ∧ digitSum [2, 7, 5] = 14 ∧ 572 % 9 = 5 ∧ 14 % 9 = 5 ∧
      572 % 3 = 2 ∧ 14 % 3 = 2 := by
  decide

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

Factor trees. Every number from $2$ on has a prime factor, and every number from $1$ on is a product of primes. The proofs are the factor-tree argument, made precise with strong induction: assume the result for all smaller numbers.

exists_prime_factorLean 4Proved here from basic factsFormally verified

/-- Every number `n ≥ 2` has a prime factor. Strong induction: if `n` is prime, it is its own
prime factor; otherwise `n = a × b` with `2 ≤ a < n`, and a prime factor of the smaller number
`a` is also a factor of `n`. -/
theorem exists_prime_factor (n : Nat) (h2 : 2 ≤ n) : ∃ p, IsPrime p ∧ p ∣ n := by
  induction n using Nat.strongRecOn with
  | _ n ih =>
    by_cases hp : IsPrime n
    · exact ⟨n, hp, Nat.dvd_refl n⟩
    · obtain ⟨a, b, ha2, han, _, _, hab⟩ := not_prime_split h2 hp
      obtain ⟨p, hpp, hpa⟩ := ih a han ha2
      exact ⟨p, hpp, Nat.dvd_trans hpa ⟨b, hab⟩⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

factorisation_existsLean 4Proved here from basic factsFormally verified

/-- Every whole number `n ≥ 1` is a product of primes (`1` is the empty product). This is the
factor tree, made precise: split any number that is not prime into two smaller factors, and
keep going. The numbers get smaller, so the splitting must stop, and then every leaf is prime.
Uniqueness of the primes (up to order) is *not* proved here. -/
theorem factorisation_exists (n : Nat) (h1 : 1 ≤ n) :
    ∃ ps : List Nat, (∀ p ∈ ps, IsPrime p) ∧ listProd ps = n := by
  induction n using Nat.strongRecOn with
  | _ n ih =>
    by_cases hn1 : n = 1
    · exact ⟨[], by simp, by simp [listProd, hn1]⟩
    · have h2 : 2 ≤ n := by omega
      by_cases hp : IsPrime n
      · exact ⟨[n], by simpa using hp, by simp [listProd]⟩
      · obtain ⟨a, b, ha2, han, hb2, hbn, hab⟩ := not_prime_split h2 hp
        obtain ⟨xs, hxs, hxa⟩ := ih a han (by omega)
        obtain ⟨ys, hys, hyb⟩ := ih b hbn (by omega)
        refine ⟨xs ++ ys, ?_, ?_⟩
        · intro p hp'
          rcases List.mem_append.mp hp' with hx | hy
          · exact hxs p hx
          · exact hys p hy
        · rw [listProd_append, hxa, hyb, hab]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

factor_tree_360Lean 4Proved here from basic factsFormally verified

/-- The factor tree in the lesson: `360 = 2 × 2 × 2 × 3 × 3 × 5`, and every leaf is prime. -/
theorem factor_tree_360 :
    listProd [2, 2, 2, 3, 3, 5] = 360 ∧ ∀ p ∈ [2, 2, 2, 3, 3, 5], IsPrime p := by
  decide

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

Uniqueness is not automatic. In the even-number world, $60$ has two different factorisations:

even_world_not_uniqueLean 4Proved here from basic factsFormally verified

/-- Unique factorisation is not automatic. In the even-number world, `2`, `6`, `10` and `30`
are all even-primes, and `60 = 6 × 10 = 2 × 30` has two *different* factorisations into
even-primes. Ordinary whole numbers never behave like this, but that needs a proof. -/
theorem even_world_not_unique :
    IsEvenPrime 2 ∧ IsEvenPrime 6 ∧ IsEvenPrime 10 ∧ IsEvenPrime 30 ∧
      60 = 6 * 10 ∧ 60 = 2 * 30 := by
  decide

Axioms used: No axiomsformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

Euclid. The proof uses $n! = 1 \times 2 \times \cdots \times n$ instead of a list of primes. Every number from $1$ to $n$ divides $n!$ , so none of them can divide $n! + 1$ except $1$ :

infinitely_many_primesLean 4Proved here from basic factsFormally verified

/-- **Euclid**: there is a prime bigger than any number `n`. Take a prime factor `p` of
`n! + 1`. If `p` were at most `n`, it would divide `n!` and `n! + 1`, hence `1`; impossible.
So `p > n`. -/
theorem infinitely_many_primes (n : Nat) : ∃ p, n < p ∧ IsPrime p := by
  have h2 : 2 ≤ fact n + 1 := by have := fact_pos n; omega
  obtain ⟨p, hp, hpd⟩ := exists_prime_factor (fact n + 1) h2
  refine ⟨p, ?_, hp⟩
  apply Classical.byContradiction
  intro hle
  have hpf : p ∣ fact n := dvd_fact (by have := hp.1; omega) (by omega)
  have h1 : p ∣ 1 := (Nat.dvd_add_right hpf).mp hpd
  have hp1 : p ≤ 1 := Nat.le_of_dvd (by decide) h1
  have hp2 : 2 ≤ p := hp.1
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

euclid_30031Lean 4Proved here from basic factsFormally verified

/-- Euclid's numbers need not be prime: `2 × 3 × 5 × 7 × 11 × 13 + 1 = 30031 = 59 × 509`.
But its prime factors `59` and `509` are new: neither is on the list `2, 3, 5, 7, 11, 13`. -/
theorem euclid_30031 : 2 * 3 * 5 * 7 * 11 * 13 + 1 = 59 * 509 ∧ IsPrime 59 ∧ IsPrime 509 := by
  -- Testing all 509 smaller numbers is a long computation, so we let Lean's kernel do it.
  decide +kernel

Axioms used: propext, Quot.soundformal/Lumenary/FactorsPrimes.leanTry it in the Lean web editor

What is not formalised here: the uniqueness of prime factorisation (the fundamental theorem of arithmetic). Lean's library Mathlib proves it, and so will a later lesson.

ComputationC

Margaret sieves and checks

Sieving primes and growing factor treesPythonExact computationExhaustive finite checkComputationally tested

"""The sieve of Eratosthenes, factor trees, and Euclid's new primes.

The sieve finds the primes up to n by crossing out multiples. We check that
crossing out multiples of the primes up to the square root of n is enough,
count how the primes thin out, split numbers into primes along two different
factor trees (the same primes appear every time we look), and factor Euclid's
numbers 2 x 3 x ... x p + 1 to see that their prime factors are always new.
"""

import math

def sieve(n, stop_at=None):
    """Primes up to n by the sieve of Eratosthenes.

    Multiples are crossed out only for primes p <= stop_at (default: all p).
    """
    if n < 2:
        return []
    alive = [False, False] + [True] * (n - 1)
    for p in range(2, n + 1):
        if stop_at is not None and p > stop_at:
            break
        if alive[p]:
            for multiple in range(2 * p, n + 1, p):
                alive[multiple] = False
    return [k for k in range(n + 1) if alive[k]]

def smallest_factor(n):
    """The smallest factor of n that is bigger than 1 (n >= 2)."""
    if n < 2:
        raise ValueError("n must be at least 2")
    for d in range(2, math.isqrt(n) + 1):
        if n % d == 0:
            return d
    return n

def tree_small_first(n):
    """Factor tree that always splits off the smallest factor; sorted leaves."""
    leaves = []
    while n > 1:
        p = smallest_factor(n)
        leaves.append(p)
        n //= p
    return leaves

def tree_middle_split(n):
    """A different factor tree: split n = a x b with a as close to sqrt(n)."""
    for a in range(math.isqrt(n), 1, -1):
        if n % a == 0:
            return sorted(tree_middle_split(a) + tree_middle_split(n // a))
    return [n] if n > 1 else []

def euclid_numbers(count):
    """(primes used, 2 x 3 x ... x p + 1, its prime factors) for the first primes."""
    primes = sieve(100)[:count]
    rows = []
    for k in range(1, count + 1):
        number = math.prod(primes[:k]) + 1
        rows.append((primes[:k], number, tree_small_first(number)))
    return rows

def main():
    small = sieve(100)
    print(f"Sieve of Eratosthenes up to 100: {len(small)} primes")
    print("  " + " ".join(map(str, small)))
    print("Crossing out multiples of 2, 3, 5 and 7 only (primes up to 10):")
    print(f"  same list? {sieve(100, stop_at=10) == small}")
    big = sieve(10_000)
    for limit in (100, 1_000, 10_000):
        count = sum(p <= limit for p in big)
        print(f"  primes up to {limit:>6,}: {count:>5,}  ({count / limit:.1%} of"
              " the numbers)")
    same = all(tree_small_first(n) == tree_middle_split(n)
               for n in range(2, 5_001))
    print()
    print("Two different factor trees for 360:")
    print(f"  smallest factor first: {' x '.join(map(str, tree_small_first(360)))}")
    print("  split 360 = 18 x 20 first: "
          f"{' x '.join(map(str, tree_middle_split(360)))}")
    print(f"  both trees give the same primes for every n from 2 to 5,000: {same}")
    print()
    print("Euclid's numbers: multiply the first primes and add 1")
    for used, number, primes in euclid_numbers(7):
        product = " x ".join(map(str, used))
        found = "prime" if len(primes) == 1 else " x ".join(map(str, primes))
        new = "new" if all(p not in used for p in primes) else "old!"
        print(f"  {product} + 1 = {number}: {found} ({new})")
    print()
    print("Epistemic status: the sieve and the factorisations are exact. Matching")
    print("factor trees for n up to 5,000 is evidence for unique factorisation,")
    print("not a proof (that comes in a later lesson). Euclid's argument proves")
    print("that the primes never run out; the table only illustrates it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Every one of the $4{,}999$ comparisons matched. That is strong evidence that factor trees always end in the same primes, but checking cases can never cover every number. That needs the proof you will meet later.

Divisibility tests, checked and brokenPythonExhaustive finite checkCounterexampleComputationally tested

"""Divisibility tests: which shortcuts work, and which only look as if they do.

The last digit decides divisibility by 2, 5 and 10; the digit sum decides
divisibility by 3 and 9. We test each rule against honest division for every
number below 100,000, then try the same shortcuts where they do not belong
(digit sum for 7, last digit for 4) and report the first counterexample.
"""

LIMIT = 100_000

def digits(n):
    """Decimal digits of n >= 0, ones digit first."""
    if n < 0:
        raise ValueError("n must be a whole number")
    out = [n % 10]
    while n >= 10:
        n //= 10
        out.append(n % 10)
    return out

def digit_sum(n):
    """Sum of the decimal digits of n."""
    return sum(digits(n))

def alternating_sum(n):
    """Ones digit minus tens digit plus hundreds digit minus ..."""
    return sum(d if k % 2 == 0 else -d for k, d in enumerate(digits(n)))

def first_failure(test, d, limit=LIMIT):
    """Smallest n < limit where test(n) disagrees with 'd divides n', or None."""
    for n in range(limit):
        if test(n) != (n % d == 0):
            return n
    return None

#: (description, divisor, shortcut test). The two marked "a guess" are not real tests.
RULES = [
    ("last digit for 2", 2, lambda n: (n % 10) % 2 == 0),
    ("last digit for 5", 5, lambda n: (n % 10) in (0, 5)),
    ("last digit for 10", 10, lambda n: n % 10 == 0),
    ("digit sum for 3", 3, lambda n: digit_sum(n) % 3 == 0),
    ("digit sum for 9", 9, lambda n: digit_sum(n) % 9 == 0),
    ("alternating sum for 11", 11, lambda n: alternating_sum(n) % 11 == 0),
    ("digit sum for 7 (a guess)", 7, lambda n: digit_sum(n) % 7 == 0),
    ("last digit for 4 (a guess)", 4, lambda n: (n % 10) % 4 == 0),
    ("last two digits for 4", 4, lambda n: (n % 100) % 4 == 0),
]

def main():
    print(f"Each shortcut against honest division, for every n below {LIMIT:,}:")
    for name, d, test in RULES:
        n = first_failure(test, d)
        if n is None:
            verdict = "agrees every time"
        else:
            says = "yes" if test(n) else "no"
            verdict = f"FAILS first at n = {n}: says {says}, but {n} % {d} = {n % d}"
        print(f"  {name:<26} {verdict}")
    print()
    print("Why the digit sum works for 9: 10 = 9 + 1, 100 = 99 + 1, ...")
    n = 572
    print(f"  {n} = 5 x 99 + 7 x 9 + ({' + '.join(map(str, digits(n)[::-1]))})"
          f" = 9 x {(5 * 99 + 7 * 9) // 9} + {digit_sum(n)}")
    print(f"  so {n} and {digit_sum(n)} leave the same remainder on division by"
          f" 9: {n % 9} and {digit_sum(n) % 9}")
    print()
    print("Epistemic status: every number below 100,000 was checked, so the real")
    print("tests are certain for those numbers and the counterexamples are")
    print("genuine; that the real tests work for all numbers is the lesson's")
    print("place-value argument, not this search.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Exercises

Your turn

Take your time. You can open a hint whenever you like.

1. Factors, multiples and primes

Warm-upHuman

List all the factors of $36$ , separated by commas.

2. Factors, multiples and primes

Warm-upHuman

Which sentence is true?

Choose one

18

is a factor of

6

6

is a multiple of

18

6

is a factor of

18

, and

18

is a multiple of

6

6

is both a factor and a multiple of

18

3. Factors, multiples and primes

Warm-upHuman

Is the number $1$ prime, composite, or neither?

Choose one

PrimeCompositeNeither

4. Factors, multiples and primes

CoreHuman

5. Factors, multiples and primes

CoreHuman

What is the greatest common factor of $24$ and $36$ ?

6. Factors, multiples and primes

CoreHuman

In Nairobi, one bus leaves the station every $4$ minutes and another every $6$ minutes. Both leave together right now. After how many minutes do they next leave together?

7. Factors, multiples and primes

CoreHuman

Which of these writes $84$ as a product of primes?

Choose one

2 \times 2 \times 3 \times 7

4 \times 3 \times 7

2 \times 42

2 \times 3 \times 14

8. Factors, multiples and primes

CoreHuman

Use the digit-sum test. Which of these numbers are divisible by $9$ ? (Choose all that apply.)

Choose all that apply

738

1234

9909

5551

9. Factors, multiples and primes

CoreFormal

Lean writes b ∣ a to mean " $b$ is a factor of $a$ ", that is, $a = b \times k$ for some $k$ . Which Lean statement says that $3$ is a factor of $12$ ?

Choose one

3 ∣ 1212 ∣ 312 % 3 = 33 * 12 = 36

10. Factors, multiples and primes

StretchComputational

Write is_prime(n) that returns True if n is prime and False otherwise. Try every possible factor d from 2 upwards, but stop as soon as d * d > n (the lesson explains why that is enough). The starter uses the mistaken idea that odd numbers are prime, so the tests fail.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Things that trip people up

Misconception

"1 is a prime number." A prime must be greater than $1$ and have exactly two factors, $1$ and itself. The number $1$ has only one factor. Leaving $1$ out also keeps factor trees unique: otherwise $6 = 2 \times 3 = 1 \times 2 \times 3 = 1 \times 1 \times 2 \times 3 = \cdots$

Misconception

"All odd numbers are prime." $9 = 3 \times 3$ , $15 = 3 \times 5$ and $21 = 3 \times 7$ are odd and composite. Being odd only tells you that $2$ is not a factor.

Misconception

"2 can't be prime, because it is even." $2$ has exactly two factors, $1$ and $2$ , so it is prime. It is the only even prime.

Misconception

Mixing up factors and multiples. The factors of $12$ are $1, 2, 3, 4, 6, 12$ : they fit into $12$ . The multiples of $12$ are $12, 24, 36, \dots$ : they are built from $12$ . A number has only a few factors but infinitely many multiples.

Misconception

"The digit-sum test works for every number." It works for $3$ and $9$ because $10 = 9 + 1$ . For $7$ it fails: $14$ is divisible by $7$ , but its digit sum $5$ is not.

ViewpointsH

Other ways of seeing

Number theory— Primes are the atoms of arithmetic

A number theorist thinks of primes as atoms: every whole number is built from them by multiplying, in exactly one way. Many questions about primes are easy to ask and very hard to answer. For example: is every even number greater than $2$ the sum of two primes ( $4 = 2 + 2$ , $10 = 3 + 7$ , $100 = 3 + 97$ )? This is Goldbach's conjecture (1742). It has been checked by computer for enormous numbers, but nobody has proved it. It is still an open problem. See number theory.

Geometry— Factors are rectangles

A geometer sees the factor pairs of $n$ as the rectangles with area $n$ and whole-number sides. A prime is a number of squares that can only be arranged as a single strip. A perfect square ( $36$ ) is one whose rectangles include a square. Common factors also have a picture: the squares of side $12$ are the biggest squares that tile a $24$ by $36$ rectangle exactly. Euclid's method for finding them is in Euclid's algorithm.

Computation— Multiplying is easy, factoring is hard

A computer can multiply two numbers with hundreds of digits in a blink. But going backwards, finding the prime factors of a huge number, seems to be extremely hard: nobody knows a fast method for ordinary computers. Much of the secret-keeping on the internet, such as the RSA system, depends on this. It is a widely held belief, not a theorem, that no fast method exists. See secret codes and cryptography.

Set-theoretic connectionH

Factors and multiples as sets

The factors of $24$ form a set, $F_{24} = \{1, 2, 3, 4, 6, 8, 12, 24\}$ , and so do the factors of $36$ . The common factors are exactly the intersection (see sets):

F_{24} \cap F_{36} = \{1, 2, 3, 4, 6, 12\}.

In a Venn diagram, the overlap holds the common factors, and the greatest common factor is the biggest number there. The multiples of $4$ and the multiples of $6$ are infinite sets. Their intersection is the set of multiples of $12$ . The set of all primes is infinite too, by Euclid's theorem.

Wonder Trails

Optional, and never graded: a question that leads somewhere further.

Wonder Trail · Optional · never gradedPrimes forever2, 3, 5, 7, 11, 13, … The primes get rarer as the numbers grow. Do they ever run out? And how rare do they get?Follow the trail

History & global context

History and global context

A puzzle from Africa. The Ishango bone, found in what is now the Democratic Republic of the Congo and roughly $20{,}000$ years old, carries groups of notches. One column has groups of $11$ , $13$ , $17$ and $19$ , the primes between $10$ and $20$ . Some people have suggested it records primes, but most researchers think this is a coincidence. Nobody knows what the notches meant.
Greece. Euclid's Elements (around 300 BCE) defines prime numbers (Book VII). Book IX contains his proof that there are more primes than any given list. Eratosthenes of Cyrene, a scholar at Alexandria in the 3rd century BCE, is credited with the sieve. The method is described by Nicomachus of Gerasa around 100 CE.
China. The Sunzi Suanjing (written between the 3rd and 5th centuries CE) asks for a number that leaves remainder $2$ when divided by $3$ , remainder $3$ when divided by $5$ and remainder $2$ when divided by $7$ . Puzzles like this one, about remainders and multiples, grew into the Chinese remainder theorem.
Germany. Carl Friedrich Gauss gave the first complete, careful proof that prime factorisations are unique in his Disquisitiones Arithmeticae (1801).
Today. Volunteers all over the world search for record-breaking primes with their computers. In October 2024 the Great Internet Mersenne Prime Search found a prime with more than $41$ million digits, the largest known at that time.

Chairs for the assembly

Rectangles of dots

The words we need

Worked examples

Explore: multiples and the sieve

Why it all works

Finding factors: when to stop

The smallest factor is always prime

Every number is built from primes

The divisibility tests

Why the sieve can stop early

The primes never run out

Gideon's precise statements

Margaret sieves and checks

Your turn

Things that trip people up

Other ways of seeing

Factors and multiples as sets

Wonder Trails

History and global context

Further reading