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. I’m a hobby mathematician learning to formalize proofs in the Lean4 language. I chose this proof as a beginner project, not knowing exactly what I went into. However, the best way to know in many occasions is to make a map. This is the reason for this blueprint.
-The aim of this formalization is to stay close to the text. It turned out that the proof needs "obvious" facts about the primes, and to show these, we cannot use Mathlib4’s set of primes, which has infinite cardinality. So, we construct FinitePrimes and prove some of their properties that we need.
-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+
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 \).
+ +Given the prime counting function \(\pi (n)\), \(n\in \mathbb {N}\), we define \(\pi _R(x)\), \(x\in \mathbb {R}\) as \(\pi _R(x) = \pi (|\lfloor x\rfloor |)\).
-In the text we use \(\pi \) in both cases, since it is clear from the domain which function is meant.
+We use Mathlib lemma log_add_one_le_harmonic which proves the inequality for \(x=n+1\).
\(\pi \) is monotone.
+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.
+For \(x\ge 3\), \(\pi (x)\ge 2\).
+ +For \(n\ge 2\),
-By algebraic manipulation around the geometric series formula (tsum_geometric_of_lt_one in Mathlib4).
For \(k,p \in \mathbb {R}\), \(k\ge 0\), \(p \ge k+1\),
+The current proof is by algebraic manipulation of fractions.
+ +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.
+ +For all \(3\le k\le \pi (x)\), the \(k\)th prime \(p_k \ge k+2\).
For \(k,p \in \mathbb {R}\), \(k\ge 0\), \(p \ge 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.
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\).
+\(\pi (x)\) is monotone.
+ +By cases and the monotonicity of \(\pi (n)\) and that of the floor function.
Given the infinite set \(S_x\) of all numbers \(m\) that have only prime factors \(p\le x\),
-For \(x\ge 3\), \(\pi (x)\ge 2\).
+ +For \(n\ge 2\),
+We transform into a product over the open interval and use the existing Mathlib4’s lemmata in an induction proof.
+ +Given the infinite set \(S_x\) of all numbers \(m\) that have only prime factors \(p\le x\),
-For \(x\ge 3\),
+By substitution into lemma 0.13.
+ +For \(n\in \mathbb {N}\), \(x\in \mathbb {R}\), \(n\le x {\lt} n+1\),
-All of the inverses in the left sum are contained in the right sum.
+ +The set \(\mathbb {P} = \big\{ p \in \mathbb {N} \ \mid \ p \ \mathrm{prime} \big\} \) has infinite cardinality.
+The set \(\mathbb {P} = \big\{ p \in \mathbb {N} \ \mid \ p \ \mathrm{prime} \big\} \) is infinite.