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' second theorem for primes
Statement
Facts & Assumptions
Given: A real number and the function
Abel summation by parts is available (Abel summation by parts: with one has for every ).
Proof
Apply [L2] to the sequence on primes and otherwise, with . Exactly as in Abel summation recovers the prime-counting function from theta, this gives
By [L1], write with . Substituting into step 1.1 yields Since , we obtain
Because is bounded and the improper integral converges, and replacing the upper limit by changes step 2.1 by only . Therefore where This constant is exactly the limit in The Meissel-Mertens constant.
The displayed asymptotic implies as , so the definition of The Meissel-Mertens constant is well posed.
Depends on
- The Meissel-Mertens constant
- Abel summation recovers the prime-counting function from theta
- 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 \ge 1$
- Mertens' first theorem for primes
- 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
Used by
- The sum of the reciprocals of the primes diverges Corollary
- A Theta(1/log x) product bound does not determine the Mertens constant Counterexample
- Numerics for the first and second Mertens theorems Example
- Mertens' third theorem for primes Theorem
Cited to discharge well-definedness by The Meissel-Mertens constant.
Dependency tree · two levels
28 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)