TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Mertens' first theorem for primes

Statement

For every real $x \geq 2$ ,

$\sum_{p \leq x} \frac{\log p}{p} = \log x + O (1) .$

Facts & Assumptions

Given: A real number $x \geq 2$ .

[L1]

The weighted von Mangoldt harmonic sum satisfies $\sum_{n \leq x} \frac{Λ (n)}{n} = \log x + O (1)$ (The von Mangoldt harmonic sum is log x plus O(1)).

[L2]

The von Mangoldt function is $Λ (p^{k}) = \log p$ on prime powers and $0$ otherwise (The von Mangoldt function, Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L3]

The real $p$ -series $\sum_{m \geq 1} m^{- 3 / 2}$ converges, and comparison for nonnegative series is valid (The p-series for a real exponent p converges exactly when p is greater than one, If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ).

[L4]

The logarithm is increasing and satisfies $\log (u v) = \log u + \log v$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

Proof

technique · direct

1.1L2givenalgebra

By [L2], $\sum_{n \leq x} \frac{Λ (n)}{n} = \sum_{p \leq x} \frac{\log p}{p} + \sum_{\begin{array}{c} p^{k} \leq x \\ k \geq 2 \end{array}} \frac{\log p}{p^{k}} .$ So it is enough to show that the prime-power tail is bounded independently of $x$ .

2.1L3L4step 1.1algebra

For $t \geq 16$ , define $h (t) : = \sqrt{t} - \log t$ . By [L4], $h^{'} (t) = \frac{1}{2 \sqrt{t}} - \frac{1}{t} = \frac{\sqrt{t} - 2}{2 t} \geq 0,$ so $h$ is increasing on $[16, \infty)$ . Since $h (16) = 4 - \log 16 > 0$ , we obtain $\log p \leq \sqrt{p}$ for every prime $p \geq 16$ . Hence $\sum_{k \geq 2} \frac{\log p}{p^{k}} \leq \frac{\log p}{p^{2}} \sum_{j \geq 0} \frac{1}{p^{j}} \leq \frac{2 \log p}{p^{2}} \leq \frac{2}{p^{3 / 2}}$ for every prime $p \geq 16$ . The finitely many primes $p < 16$ contribute only a constant, so [L3] shows that $\sum_{p^{k} \leq x, k \geq 2} \frac{\log p}{p^{k}} = O (1) .$

3.1L1step 1.1step 2.1algebra∎

Combine step 2.1 with [L1]: $\log x + O (1) = \sum_{n \leq x} \frac{Λ (n)}{n} = \sum_{p \leq x} \frac{\log p}{p} + O (1) .$ Therefore $\sum_{p \leq x} \frac{\log p}{p} = \log x + O (1) .$

Depends on

Used by

Numerics for the first and second Mertens theorems Example
Mertens sum for primes in an arithmetic progression Theorem
Mertens' second theorem for primes Theorem
Mertens' third theorem for primes Theorem

Dependency tree · two levels

51 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Leo Goldmakher, A Quick Proof of Mertens' Theorem (standard reference, not scraped)
MIT 18.785 Number Theory I, Fall 2021, Problem Set 9 (standard reference, not scraped)
Victor Shoup, A Computational Introduction to Number Theory and Algebra, Version 2 (standard reference, not scraped)