TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05

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 sum for primes in an arithmetic progression

Statement

For fixed $q \geq 1$ and $(a, q) = 1$ ,

$\sum_{\begin{array}{c} p \leq x \\ p \equiv a (q) \end{array}} \frac{1}{p} = \frac{1}{φ (q)} \log \log x + O_{q} (1) .$

Facts & Assumptions

Given: A modulus $q \geq 1$ , a reduced residue class $a$ , and the weighted sum

$A (x) : = \sum_{\begin{array}{c} p \leq x \\ p \equiv a (q) \end{array}} \frac{\log p}{p} .$

[L1]

Character orthogonality isolates one reduced residue class modulo $q$ (Orthogonality relations for Dirichlet characters modulo q).

[L2]

For a nonprincipal character, the partial sums of $χ$ are bounded, the series $\sum_{n \geq 1} χ (n) / n$ converges to $L (1, χ)$ , and $L (1, χ) \neq 0$ (Nonprincipal Dirichlet character partial sums are bounded, Nonprincipal Dirichlet L-functions are holomorphic on Re s greater than 0, Nonprincipal Dirichlet L-functions are nonzero at one).

[L3]

The von Mangoldt identity is $\log n = \sum_{d ∣ n} Λ (d)$ , and $Λ$ is supported on prime powers (The divisor sum of von Mangoldt is the arithmetic-function logarithm, The von Mangoldt function).

[L4]

Chebyshev's bounds and the prime-power expansion imply $ψ (x) = \sum_{n \leq x} Λ (n) = O (x)$ (Chebyshev's psi function, Prime-power expansion of Chebyshev's psi function, Psi and theta differ by at most a square-root term, Chebyshev's theta function has linear lower and upper bounds).

[L5]

The ordinary weighted prime sum satisfies $\sum_{p \leq x} (\log p) / p = \log x + O (1)$ (Mertens' first theorem for primes), and Abel summation by parts is available (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ ).

Proof

technique · direct

1.1

For each Dirichlet character $χ$ modulo $q$ , define $A_{χ} (x) : = \sum_{p \leq x} χ (p) \frac{\log p}{p} .$ Because every prime $p \equiv a (m o d q)$ is coprime to $q$ , [L1] gives $φ (q) A (x) = \sum_{χ m o d q} \overline{χ (a)} A_{χ} (x) .$

L1givenalgebra

2.1

If $χ = χ_{0}$ is principal, then $A_{χ_{0}} (x) = \sum_{\begin{array}{c} p \leq x \\ p ∤ q \end{array}} \frac{\log p}{p} = \log x + O_{q} (1)$ by [L5]. Now let $χ \neq χ_{0}$ , put $M_{χ} (y) : = \sum_{n \leq y} χ (n)$ , and define $T_{χ} (x) : = \sum_{n \leq x} \frac{χ (n) \log n}{n}, S_{χ} (x) : = \sum_{n \leq x} \frac{χ (n) Λ (n)}{n} .$ Abel summation and [L2] give $T_{χ} (x) = O_{q} (1)$ and $\sum_{b \leq y} \frac{χ (b)}{b} = L (1, χ) + O_{q} (y^{- 1}) .$ Using [L3], complete multiplicativity, and finite rearrangement, $T_{χ} (x) = \sum_{a \leq x} \frac{χ (a) Λ (a)}{a} \sum_{b \leq x / a} \frac{χ (b)}{b} = L (1, χ) S_{χ} (x) + O_{q} ⁣ (\frac{1}{x} \sum_{a \leq x} Λ (a)) .$ The last error is $O_{q} (1)$ by [L4]. Since $L (1, χ) \neq 0$ by [L2], it follows that $S_{χ} (x) = O_{q} (1)$ . Removing the absolutely bounded contribution of prime powers $p^{m}$ with $m \geq 2$ gives $A_{χ} (x) = O_{q} (1)$ . Returning to step 1.1, only the principal character contributes an unbounded term, and therefore $A (x) = \frac{1}{φ (q)} \log x + O_{q} (1) .$

L2L3L4L5step 1.1algebra

3.1

Apply [L5] to the sequence that is $1 / p$ on primes $p \equiv a (m o d q)$ and $0$ otherwise, with weight $\log n$ . Exactly as in the ordinary prime Mertens argument, this gives $\sum_{\begin{array}{c} p \leq x \\ p \equiv a (q) \end{array}} \frac{1}{p} = \frac{A (x)}{\log x} + \int_{2}^{x} \frac{A (t)}{t \log^{2} t} d t .$ Substituting the estimate from step 2.1 yields $\frac{A (x)}{\log x} = \frac{1}{φ (q)} + O_{q} ⁣ (\frac{1}{\log x})$ and $\int_{2}^{x} \frac{A (t)}{t \log^{2} t} d t = \frac{1}{φ (q)} \int_{2}^{x} \frac{d t}{t \log t} + O_{q} ⁣ (\int_{2}^{\infty} \frac{d t}{t \log^{2} t}) = \frac{1}{φ (q)} \log \log x + O_{q} (1) .$ Combining these two estimates proves $\sum_{\begin{array}{c} p \leq x \\ p \equiv a (q) \end{array}} \frac{1}{p} = \frac{1}{φ (q)} \log \log x + O_{q} (1) .$

L5step 2.1algebra∎

Depends on

Used by

Dirichlet's theorem on primes in arithmetic progressions Theorem

Dependency tree · two levels

44 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

Kiran S. Kedlaya, Notes on Analytic Number Theory, Chapter 4 (standard reference, not scraped)
P. Andersen, Analytic Number Theory, Chapters 14-15 (standard reference, not scraped)