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

Chebyshev bounds for the prime-counting function

Statement

There exist positive constants c1<c2 and a real number x0 such that

c1xlog⁡x≤π(x)≤c2xlog⁡x

for every real x≥x0.

Facts & Assumptions

Given: A real number x≥2.

[L1]

For every real x≥2, π(x)=θ(x)log⁡x+∫2xθ(t)tlog⁡2t dt (Abel summation recovers the prime-counting function from theta).

[L2]

Chebyshev's theta function has positive linear lower and upper bounds for sufficiently large arguments (Chebyshev's theta function has linear lower and upper bounds).

[L3]

The prime-counting and theta functions are the ones defined in The prime-counting function and Chebyshev's theta function.

Proof

technique · direct
1.1L2L3choose

By [L2], choose positive constants a,b and y0≥2 such that at≤θ(t)≤bt for every t≥y0. Enlarging b if needed to absorb the finite range 2≤t≤y0, we may assume θ(t)≤bt(t≥2).

2.1L1step 1.1algebra

For x≥y0, the integral term in [L1] is nonnegative, so π(x)≥θ(x)log⁡x≥axlog⁡x.

2.2L1step 1.1givenalgebra

Assume now that x≥max⁡{y02,e2}. Using [L1] and step 1.1, π(x)≤bxlog⁡x+b∫2xdtlog⁡2t. Split the integral at x. On [2,x] one has log⁡t≥log⁡2, so ∫2xdtlog⁡2t≤xlog⁡22<3x. On [x,x] one has log⁡t≥12log⁡x, so ∫xxdtlog⁡2t≤4xlog⁡2x. Hence π(x)≤bxlog⁡x+3bx+4bxlog⁡2x.

3.1step 2.1step 2.2choosealgebra∎

Since x=o(x/log⁡x) and x/log⁡2x≤x/log⁡x for x≥e, step 2.2 implies π(x)≤c2xlog⁡x for some positive constant c2 and all sufficiently large x. Taking c1=a and enlarging x0 if necessary to satisfy both steps 2.1 and 2.2 proves the theorem.

Depends on

Used by

Dependency tree · two levels

14 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