Existing in Mathlib · Number theory
Divergence of the Reciprocal-Prime Series
The real family that assigns the reciprocal 1/p to every prime p cannot have a finite sum.
- reciprocals of primes
- nonsummable families
- smooth numbers
- rough numbers
- vanishing tails
Exact theorem
Exact Mathlib statement
theorem Nat.Primes.not_summable_one_div : ¬ Summable (fun p : Nat.Primes ↦ (1 / p : ℝ))The theorem at a glance
Divergence of Prime Reciprocals — a nonvanishing tail
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Divergence of Prime Reciprocals — a nonvanishing tail
Detailed visual description
The exact subtype-indexed conclusion leads into the checked Erdős route: split bounded naturals into smooth and rough parts, control the smooth part by a square-root estimate, charge the rough part to primes beyond one cutoff, and repeat the visible tail-basin mechanism beyond a farther cutoff. The second gate makes the obstruction to summable tails explicit rather than presenting one isolated finite sum.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Reciprocal-prime mass beyond receding cutoffs — scientific schematic
Detailed visual description
Green facets stand for primes, gold disks for reciprocal contributions, and nested blue arcs for successively farther cutoffs. Contributions become individually smaller and sparser but remain visibly present beyond each cutoff. The schematic expresses the nonvanishing-tail obstruction behind nonsummability of the subtype-indexed family p ↦ 1/p. It does not depict an ordered partial-sum limit, a divergence rate, a prime-counting asymptotic, or prime-spacing information.
Why it matters
A mathematical landmark
Euler's theorem that the sum of prime reciprocals diverges is a classical bridge between elementary series and the distribution of primes. Mathlib retains a particularly visual Erdős proof in which smooth and rough number counts force a uniform lower bound on arbitrarily remote finite prime tails.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's order-independent subtype form: the real-valued family p ↦ 1/p on Nat.Primes is not Summable. The declaration is not literally phrased as convergence of ordered partial sums to +∞, and it supplies no divergence rate or asymptotic estimate.
- The exact endpoint is nonsummability over the subtype Nat.Primes, independent of any chosen enumeration.
- The declaration is not literally a statement that one ordered sequence of partial sums tends to +∞.
- It gives no quantitative divergence rate, asymptotic formula, or estimate for the prime-counting function.
- ProofAtlas is indexing an existing Mathlib theorem, not claiming new mathematics.
Source and local evidence
Where the theorem comes from
- Existing declaration
Nat.Primes.not_summable_one_divin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.divergence-prime-reciprocal-series.v001