Infinite primes via log(x)

Moritz Firsching, Ralf Stephan

The proof of the infinitude of primes via the fact that $\log x\le \pi (x)+1$ is the fourth proof of this theorem in Aigner & Ziegler’s "Proofs from THE BOOK", and attributed to Euler. The aim of this formalization is to stay close to the text of the 6th edition of "Proofs from THE BOOK".

The orginal argument by Euler(E72) involves divergent infinite sums and, so, does not satisfy modern standards of rigor(San2006).

(E72) Euler, Leonhard, Variae observationes circa series infinitas, Commentarii academiae scientiarum Petropolitanae 9 (1737), 1744, p. 160-188. Reprinted in Opera Omnia Series I volume 14, p. 216-244. Also available on line at www.EulerArchive.org.

(San2006) Sandifer, Ed, How Euler Did It, Infinitely many primes, March 2006,

http://eulerarchive.maa.org/hedi/HEDI-2006-03.pdf

Definition 0.1

In the following, the variables $n\in \mathbb {N}$, $x\in \mathbb {R}$, always satisfy $x\ge 1$, $n\le x {\lt} n+1$, which is equivalent to $n=\lfloor x\rfloor $.

Lemma 0.2

✓

\[ \log x \le \sum _{i=1}^n\frac1i. \]

Proof ▶

We use Mathlib lemma log_add_one_le_harmonic which proves the inequality for $x=n+1$.

Definition 0.3

✓

\[ S_x = \{ 1\} \ \cup \ \{ m\, \big|\, \text{$m$ has only prime factors $p\le x$}\} \]

\[ = \text{the $(\lfloor x\rfloor +1)$- or $(n+1)$-smooth numbers} \]

In Lean Mathlib, $n$-smooth numbers are defined as numbers all of whose prime factors are less than $n$. So, in the Lean proofs, a shift to $(n+1)$-smooth numbers is necessary.

To show that the sum of inverses of up to $n$ is less than the sum of inverses of all $(n+1)$-smooth numbers, it is formally necessary to first show that the second sum converges. Since the proof computes a bound for that sum anyway, we just change the order of dependent steps by determining the value of the bound, thus proving convergence, and finally comparing both sums.

Lemma 0.4

✓

\[ \sum _{m\in S_x}\frac{1}{m} = \underset {p\le x}{\prod _{p\in \mathbb {P}}}\Big(\sum _{k\in \mathbb {N}}\frac{1}{p^k}\Big). \]

Lemma 0.5

✓

\[ \underset {p\le x}{\prod _{p\in \mathbb {P}}}\Big(\sum _{k\in \mathbb {N}}\frac{1}{p^k}\Big) = \underset {p\le x}{\prod _{p\in \mathbb {P}}}\frac{p}{p-1} \]

Proof ▶

By algebraic manipulation around the geometric series formula (tsum_geometric_of_lt_one in Mathlib4).

Lemma 0.6

✓

For $k,p \in \mathbb {R}$, $k\ge 0$, $p \ge k+1$,

\[ \frac{p}{p-1} \le \frac{k+1}{k}. \]

Proof ▶

The current proof is by algebraic manipulation of fractions.

Definition 0.7

Given the prime counting function $\pi (n)$, $n\in \mathbb {N}$, we define $\pi (x)$, $x\in \mathbb {R}$ as $\pi (x) = \pi (|\lfloor x\rfloor |)$ for $x\ge 2$, and $0$ otherwise.

Lemma 0.8

✓

For all $3\le k\le \pi (x)$, the $k$th prime $p_k \ge k+2$.

Lemma 0.9

✓

\[ \underset {p\le x}{\prod _{p\in \mathbb {P}}}\frac{p}{p-1} = \prod _{k=1}^{\pi (x)}\frac{p_k}{p_k-1}. \]

From here on, we start indices under the displayed products with $1$, but use $0$ as start in the Lean proofs, also because $p_0=2$ in Lean.

Lemma 0.10

\[ \prod _{k=1}^{\pi (x)}\frac{p_k}{p_k-1} \le \prod _{k=1}^{\pi (x)}\frac{k+1}{k}. \]

This lemma needs lemma 0.6 which has the condition $p\ge k+1$ that we provide with lemma 0.8. Since $k$ is never greater than $\pi (p)$, we don’t need to assume there exist primes greater those we use in the product, i.e., $p\le x$.

Lemma 0.11

✓

$\pi (x)$ is monotone.

Proof ▶

By cases and the monotonicity of $\pi (n)$ and that of the floor function.

Lemma 0.12

✓

For $n\ge 2$,

\[ \prod _{k=1}^{n}\frac{k+1}{k} = n+1. \]

Proof ▶

We transform into a product over the open interval and use the existing Mathlib4’s lemmata in an induction proof.

Lemma 0.13

✓

For $x\ge 3$,

\[ \prod _{k=1}^{\pi (x)}\frac{k+1}{k} = \pi (x)+1. \]

Proof ▶

By substitution into lemma 0.12.

Lemma 0.14

\[ \sum _{k=1}^n\frac1k \le \sum _{m\in S_x}\frac{1}{m}. \]

Proof ▶

All of the inverses in the left sum are contained in the right sum.

Theorem 0.15

✓

For $x\in \mathbb {R}$, $\log x \le \pi (x) +1$.

Theorem 0.16

✓

The prime counting function in the real domain, $\pi :\ \mathbb {R} \mapsto \mathbb {N} \ := \# \big\{ p\mid p \in \mathbb {P}, p\le x \big\} $ is unbounded above.

Theorem 0.17

✓

The set $\mathbb {P} = \big\{ p \in \mathbb {N} \ \mid \ p \ \mathrm{prime} \big\} $ is infinite.