Alphabeta Math
LemmaStatement: 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.

Abel summation recovers the prime-counting function from theta

Statement

For every real x≥2,

π(x)=θ(x)log⁡x+∫2xθ(t)tlog⁡2t dt.

Facts & Assumptions

Given: A real number x≥2 and N:=⌊x⌋.

[L1]

By definition, π(N)=∑2≤n≤Nn prime1 (The prime-counting function).

[L2]

By definition, θ(N)=∑2≤n≤Nn primelog⁡n (Chebyshev's theta function).

[L3]

Abel summation by parts converts a finite sum ∑akbk into a boundary term plus a sum against the differences bk+1−bk (Abel summation by parts: with An=∑k<nak one has ∑k<nakbk=Anbn−1−∑k<n−1Ak+1 (bk+1−bk) for every n≥1).

[L4]

For t>1, ddt1log⁡t=−1tlog⁡2t, and log⁡(xy)=log⁡x+log⁡y with log⁡1=0 (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.1L1L2givenconstruct

Define a sequence by an=log⁡n when n is prime and an=0 otherwise, for 2≤n≤N. Then [L2] shows that its partial sums satisfy Am:=∑2≤n≤man=θ(m) for every integer m∈[2,N], while [L1] gives ∑2≤n≤Nanlog⁡n=π(N).

2.1L3step 1.1

Apply [L3] to the finite sum in step 1.1 with bn=1/log⁡n. This yields π(N)=θ(N)log⁡N−∑n=2N−1θ(n)(1log⁡(n+1)−1log⁡n).

3.1L4step 2.1algebra

For each integer n with 2≤n≤N−1, the function f(t)=1/log⁡t has derivative given by [L4], so 1log⁡(n+1)−1log⁡n=∫nn+1f′(t) dt=−∫nn+1dttlog⁡2t. Since θ(t)=θ(n) on [n,n+1), step 2.1 becomes π(N)=θ(N)log⁡N+∫2Nθ(t)tlog⁡2t dt.

4.1L4step 3.1givenalgebra∎

Because N=⌊x⌋, there are no integers in (N,x]. Hence π(x)=π(N) and θ(t)=θ(N)=θ(x) for every t∈[N,x]. Using [L4], we compute ∫Nxθ(t)tlog⁡2t dt=θ(x)∫Nxdttlog⁡2t=θ(x)(1log⁡N−1log⁡x). Adding this identity to step 3.1 gives π(x)=π(N)=θ(x)log⁡x+∫2xθ(t)tlog⁡2t dt.

Depends on

Used by

Dependency tree · two levels

21 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