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

Classical Zero Free Region and the Prime Number Theorem

1 · Prerequisites

2 · Summary

The Hadamard product and the nonnegative trigonometric polynomial give the classical zero-free region 1β1/log(γ+3). Pole-subtracted logarithmic-derivative estimates control low heights. Balancing a truncated explicit formula at T=exp(alogx) yields ψ(x)=x+O(xeclogx), followed by the corresponding theta and logarithmic-integral estimates.

The second route proves the Newman–Zagier Tauberian theorem by damped contours and then recovers a monotone counting function from its convergent integral. For arithmetic progressions the modulus is fixed: character sums are combined into a nonnegative residue-class sum before desmoothing. No region uniform in the modulus is asserted.

3 · Logical flowchart

4 · Definitions, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta logarithmic derivative zero bound

Statement

Write s=σ+it and let ρ range over nontrivial zeta zeros with multiplicity. With the Hadamard constant B, ζζ(s)=B+ρ(1sρ+1ρ)1s1+logπ2Γ(1+s/2)2Γ(1+s/2). This is a meromorphic identity, using convergent genus-one terms. Uniformly for 1σ2, t3 and ζ(s)0, Reζζ(s)=ρRe1sρ12logt+O(1), and this real series is absolutely convergent.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

The Riemann xi function has its genus-one Hadamard product over the nontrivial zeros of zeta: There exist constants A,BC such that ξ(s)=eA+BsρE1(s/ρ), where the product runs over the nontrivial zeros ρ of ζ, counted with multiplicity, and E1(w)=(1w)ew. The product converges in the genus-one canonical sense.

[F2]

The Riemann xi function ξ(s)=12s(s1)Λ(s): The completed function extends meromorphically with simple poles at 0 and 1 by thm-completed-riemann-zeta-functional-equation. The Riemann xi function is defined on C by ξ(s):=12s(s1)Λ(s)=12s(s1)πs/2Γ(s/2)ζ(s). The role of the factor 12s(s1) is to cancel the two simple poles of the completed function Λ. Thus ξ is the entire completion, while Λ remains meromorphic.

[F3]

Stirling's formula for Gamma: Fix δ with 0<δ<π. On the closed sector argzπδ, using the principal logarithm in zz1/2:=exp((z1/2)Logz), one has Γ(z)=2πzz1/2ez(1+Oδ(z1)) as z.

[F4]

All higher complex derivatives exist and satisfy Cauchy's integral formula on an interior circle: Let f be holomorphic on D(a,R), let 0<r<R, and let γ(t)=a+rexp(it) for 0t2π. Define f(0)=f and, whenever it exists, f(n+1)=(f(n)). Then every f(n) exists on D(a,r) and, for every zD(a,r) and nN, f(n)(z)=n!2πiγf(ζ)(ζz)n+1dζ. In particular, every holomorphic function has complex derivatives of all orders locally.

[F5]

A unit-interval bound for zeta zeros: The number of nontrivial zeta zeros, with multiplicity, whose ordinates lie in [T,T+1] is O(log(T+2)) for T0.

[F6]

The only zeros of zeta on the nonpositive real axis are the negative even integers, and every other zero lies in the open critical strip: For each integer m1, ζ(2m)=0. These are the only zeros of ζ on the nonpositive real axis. Every other zero ρ of ζ satisfies 0<Reρ<1. Moreover, if ρ is a nontrivial zero, then so are 1ρ and ρ.

Proof

1.1

For bounded s away from zeros, the terms 1/(sρ)+1/ρ are Os(ρ2). The unit-interval count, reflected using conjugate zeros, makes their tails normally convergent. Logarithmically differentiating the canonical product therefore gives ξ/ξ=B+ρ(1/(sρ)+1/ρ).

F1F5F6
1.2

Put z=1+s/2. In a wider fixed sector containing these high-height points, Stirling gives Γ(z)=2πexp((z1/2)Logzz)(1+r(z)) with r(z)=O(z1). On discs of radius ϵz in that sector, Cauchy gives r(z)=O(z2). Thus Γ/Γ(z)=Logz1/(2z)+O(z2), whose real part is logtlog2+O(1/t). Remaining bounded heights are compact.

F3F4
2.1

In the defining formula for ξ, use Γ(1+s/2)=(s/2)Γ(s/2) to write ξ=(s1)πs/2Γ(1+s/2)ζ(s). The Gamma recurrence follows by integration by parts on its defining integral and meromorphic continuation. Differentiating this equality proves the first formula wherever its factors are nonzero, hence meromorphically.

F2step 1.1algebra
3.1

For fixed s the real summands have tails Os(Imρ2), since 0<Reρ<1. The same estimate applies to Re(1/ρ). Their absolute convergence follows from the unit-band count. Absorb the constant ReB+Re(1/ρ) and the bounded pole term into O(1), obtaining the second formula.

F5F6step 2.1step 1.2
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta three four one logarithmic derivative inequality

Statement

For σ>1 and tR, 3ζ(σ)ζ(σ)4Reζ(σ+it)ζ(σ+it)Reζ(σ+2it)ζ(σ+2it)0.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

The logarithmic derivative of the zeta Dirichlet series is the Dirichlet series of the von Mangoldt function on Re s greater than 1: For s>1, if ζ(s):=n1ns, then ζ(s)ζ(s)=n1Λ(n)ns.

Proof

1.1

The negative logarithmic derivative has coefficients Λ(n)0. Its series is absolutely convergent for σ>1 (also Λ(n)logn), so the displayed expression equals n1Λ(n)nσ[3+4cos(tlogn)+cos(2tlogn)].

F1
2.1

For real u, 3+4cosu+cos(2u)=2(1+cosu)20. Every summand is nonnegative, so the convergent sum is nonnegative.

step 1.1algebra
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Riemann zeta classical zero free region

Statement

There is an absolute c0>0 such that ζ has no zeros in σ1c0/log(t+2). The pole at s=1 is not a zero.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Zeta logarithmic derivative zero bound: Write s=σ+it and let ρ range over nontrivial zeta zeros with multiplicity. With the Hadamard constant B, ζζ(s)=B+ρ(1sρ+1ρ)1s1+logπ2Γ(1+s/2)2Γ(1+s/2). This is a meromorphic identity, using convergent genus-one terms. Uniformly for 1σ2, t3 and ζ(s)0, Reζζ(s)=ρRe1sρ12logt+O(1), and this real series is absolutely convergent.

[F2]

Zeta three four one logarithmic derivative inequality: For σ>1 and tR, 3ζ(σ)ζ(σ)4Reζ(σ+it)ζ(σ+it)Reζ(σ+2it)ζ(σ+2it)0.

[F3]

The Riemann zeta function has no zeros on the closed half-plane Res1, except for its pole at 1: The meromorphic continuation of ζ has no zeros on the closed half-plane Res1. Its only singularity there is the simple pole at s=1.

[F4]

For Res>0, zeta admits the fractional-part integral formula with a simple residue-one pole at 1: For every complex number s with Res>0 and s1, ζ(s)=ss1s1{x}xs1dx, where {x}=xx is the fractional part. The integral defines a holomorphic function on Res>0, so the right-hand side is meromorphic there with a single simple pole at s=1 of residue 1.

Proof

1.1

For 1<σ2, the simple pole gives ζ/ζ(σ)=1/(σ1)+O(1). If ρ0=β+iγ is a zero with γ3, positivity of the real zero summands gives Re(ζ/ζ)(σ+iγ)1 ⁣C1log(γ+2)1/(σβ) and Re(ζ/ζ)(σ+2iγ)C1log(γ+2).

F1F4
2.1

Insert these bounds in the three-four-one inequality. For an absolute C1, put L=log(γ+2); then 4/(σβ)3/(σ1)+CL. Taking σ1=1/(2CL) yields 1β1/(14CL). Choosing a strictly smaller constant excludes even the closed boundary of the claimed high-height region.

F2step 1.1
3.1

The function h(s)=(s1)ζ(s) is holomorphic near the compact segment {1+it:t3}, nonzero there, and h(1)=1. Finitely many nonvanishing neighborhoods cover this segment and contain a uniform thin rectangle about it. Shrink c0 so the proposed bounded-height region to the left of one lies in that rectangle. To the right use the already proved zero-free half-plane. This proves the claim at every height, including zero.

F3F4step 2.1
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta horizontal logarithmic derivative comparison

Statement

There are absolute d>0,C>0, with d<c0, such that for t3 and σ1d/log(t+2), ζ(σ+it)ζ(σ+it)Clog(t+2).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Riemann zeta classical zero free region: There is an absolute c0>0 such that ζ has no zeros in σ1c0/log(t+2). The pole at s=1 is not a zero.

[F2]

A local formula for the logarithmic derivative of zeta: Uniformly for 1σ2 and s=σ+it1 whose ordinate is not that of a nontrivial zero, ζζ(s)=1s1+ρ:tρ<11sρ+O(log(t+2)), where zeros occur with multiplicity. For t2 the pole term is absorbed into the error, giving the usual large-height local formula.

[F3]

Zeta logarithmic derivative zero bound: Write s=σ+it and let ρ range over nontrivial zeta zeros with multiplicity. With the Hadamard constant B, ζζ(s)=B+ρ(1sρ+1ρ)1s1+logπ2Γ(1+s/2)2Γ(1+s/2). This is a meromorphic identity, using convergent genus-one terms. Uniformly for 1σ2, t3 and ζ(s)0, Reζζ(s)=ρRe1sρ12logt+O(1), and this real series is absolutely convergent.

[F4]

The logarithmic derivative of the zeta Dirichlet series is the Dirichlet series of the von Mangoldt function on Re s greater than 1: For s>1, if ζ(s):=n1ns, then ζ(s)ζ(s)=n1Λ(n)ns.

Proof

1.1

Put L=log(t+2), s1=1+L1+it. The Euler series and the real-axis simple-pole expansion give ζ/ζ(s1)ζ/ζ(1+L1)=O(L). The same comparison holds for every σ1+L1; for σ2 it is even bounded by the convergent series at two. The real-part formula now gives ρRe(1/(s1ρ))=O(L), all summands being positive.

F3F4
1.2

For Imρt1, the region theorem implies 1Reρc0/(KL) with an absolute K, since log(Imρ+2)KL. Choose d<c0/(2K). For 1d/Lσ1+1/L, the positive real parts of sρ and s1ρ are comparable, hence sρcs1ρ. Consequently 1/(sρ)1/(s1ρ)C/(Ls1ρ2)CRe(1/(s1ρ)).

F1algebra
2.1

For ordinates off the zero ordinates, subtract the two local logarithmic-derivative formulas. Their pole terms are bounded at these heights. Sum the preceding comparison over the common local zero set and use its positive-sum bound to obtain O(L). The constants do not depend on the distance of t from an ordinate. Taking limits from non-ordinates extends the bound to all t, because the entire horizontal segment is zero-free. Together with the Euler-series range this proves the assertion.

F2step 1.1step 1.2
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta bounds in classical zero free region

Statement

There are 0<c2<c1<c0 and C>0 such that for t3 and σ1c1/log(t+2), ζ/ζ(σ+it)Clog(t+2)Clog2(t+2). In the narrower c2 region, 1/ζ(s)Clog(t+2). For t3 and 1c2/log(t+2)σ2, ζ/ζ(s)+1/(s1)=O(1),1/ζ(s)=O(s1), with removable interpretations at one.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Zeta horizontal logarithmic derivative comparison: There are absolute d>0,C>0, with d<c0, such that for t3 and σ1d/log(t+2), ζ(σ+it)ζ(σ+it)Clog(t+2).

[F2]

Riemann zeta classical zero free region: There is an absolute c0>0 such that ζ has no zeros in σ1c0/log(t+2). The pole at s=1 is not a zero.

[F3]

The Riemann zeta function has its Euler product on the half-plane Res>1: For every sC with Res>1, ζ(s)=p11ps, where the product ranges over the primes and converges absolutely and locally uniformly on Res>1.

[F4]

For Res>0, zeta admits the fractional-part integral formula with a simple residue-one pole at 1: For every complex number s with Res>0 and s1, ζ(s)=ss1s1{x}xs1dx, where {x}=xx is the fractional part. The integral defines a holomorphic function on Res>0, so the right-hand side is meromorphic there with a single simple pole at s=1 of residue 1.

Proof

1.1

Choose c1 smaller than the constant in the horizontal comparison. This gives the stated derivative bound throughout the high-height region.

F1
2.1

At s1=1+1/L+it, L=log(t+2), the Euler logarithm satisfies logζ(s1)logζ(1+1/L)log(1+L), by comparing the positive real zeta series to its integral. Integrate ζ/ζ from s1 horizontally to s for 1c2/Lσ1+1/L. The length is O(1/L) and the integrand is O(L), so the change in the continued logarithm is O(1). Exponentiating its negative real part gives 1/ζ(s)=O(L). For larger sigma the Euler logarithm already gives that bound.

F3step 1.1
3.1

On the compact low-height portion choose c2<c1 sufficiently small that h(s)=(s1)ζ(s) is holomorphic and nonvanishing on a neighborhood, including h(1)=1. Then h/h and 1/h are bounded there. The identities ζ/ζ+1/(s1)=h/h and 1/ζ=(s1)/h prove both low-height estimates and their removable interpretations.

F2F4
CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta zero count near the one line

Statement

For tR and 0<r3/4, let n(r;t) count nontrivial zeros with ρ(1+it)r, including multiplicity. Then n(r;t)=O(rlog(t+2)), uniformly.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Riemann zeta classical zero free region: There is an absolute c0>0 such that ζ has no zeros in σ1c0/log(t+2). The pole at s=1 is not a zero.

[F2]

Zeta logarithmic derivative zero bound: Write s=σ+it and let ρ range over nontrivial zeta zeros with multiplicity. With the Hadamard constant B, ζζ(s)=B+ρ(1sρ+1ρ)1s1+logπ2Γ(1+s/2)2Γ(1+s/2). This is a meromorphic identity, using convergent genus-one terms. Uniformly for 1σ2, t3 and ζ(s)0, Reζζ(s)=ρRe1sρ12logt+O(1), and this real series is absolutely convergent.

[F3]

The logarithmic derivative of the zeta Dirichlet series is the Dirichlet series of the von Mangoldt function on Re s greater than 1: For s>1, if ζ(s):=n1ns, then ζ(s)ζ(s)=n1Λ(n)ns.

[F4]

A unit-interval bound for zeta zeros: The number of nontrivial zeta zeros, with multiplicity, whose ordinates lie in [T,T+1] is O(log(T+2)) for T0.

Proof

1.1

Write L=log(t+2). For a sufficiently small absolute a>0, r<a/L makes the disc zero-free: within it log(Imρ+2)KL, whereas 1Reρr. This contradicts the region bound if a zero occurs.

F1
2.1

For t3 and a/Lr1/6, evaluate at s1=1+r+it. The Euler series gives ζ/ζ(s1)=O(1/r), using its simple-pole expansion on the real axis. The positive real zero sum is thus O(1/r+L). Every counted zero contributes at least r/(4r2+r2)=1/(5r), since its real separation is between r and 2r and its imaginary separation at most r. Hence n(r;t)=O(1+rL)=O(rL).

F2F3step 1.1
3.1

If r1/6 and t3, finitely many adjacent unit ordinate bands give n(r;t)=O(L)=O(rL). Negative bands have the same count by conjugation of zeta. For t3, all counted zeros lie in one compact rectangle and are finite in number, while a nonempty disc must have ra/La/log5. Enlarging the constant handles these remaining cases.

F4step 1.1
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta reciprocal zero sum bound

Statement

For T2, the sum of 1/ρ over nontrivial zeros with 0<ImρT is O(log2T), with multiplicity. Adjoining any real nontrivial zeros preserves the estimate.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

A unit-interval bound for zeta zeros: The number of nontrivial zeta zeros, with multiplicity, whose ordinates lie in [T,T+1] is O(log(T+2)) for T0.

[F2]

The Riemann zeta zero-counting function: For T>0, N(T) is the number, with multiplicity, of nontrivial zeros ρ=β+iγ of the meromorphic continuation of zeta satisfying 0<γT. Thus a zero on the top boundary is included.

[F3]

The Riemann xi function has its genus-one Hadamard product over the nontrivial zeros of zeta: There exist constants A,BC such that ξ(s)=eA+BsρE1(s/ρ), where the product runs over the nontrivial zeros ρ of ζ, counted with multiplicity, and E1(w)=(1w)ew. The product converges in the genus-one canonical sense.

Proof

1.1

Nontrivial zeros have no accumulation in a compact subset of the plane. The finitely many with Imρ1 have nonzero denominator: the product for xi has no zero at zero, and its factors have exactly the nontrivial zeros. Their reciprocal sum is a fixed finite constant.

F3
2.1

For each integer n1, zeros with nImρn+1 each contribute at most 1/n. The count in either band is O(log(n+2)); the negative band follows from ζ(s)=ζ(s), first on its defining half-plane and then by continuation. Therefore the remaining sum is at most CnTlog(n+2)/n=O(log2T). Endpoint overlap only increases this upper bound.

F1F2step 1.1
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Zeta explicit formula zero free error balance

Statement

For x2 and finite T3, the classical region and truncated explicit formula give ψ(x)x=O(xec0logx/log(T+2)log2T+xlog2(xT)T+logx). Constants may be enlarged and the positive region constant decreased. The zero sum used in the proof is finite.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

The truncated von Mangoldt explicit formula: For x,T2, ψ0(x)x=ρ<Txρρζ(0)ζ(0)12log(1x2)+O ⁣(xlog2(xT)T+(logx)min{1,xTx}), where x is the distance to the nearest prime power other than possibly x. The zero sum is finite and counts multiplicities.

[F2]

Riemann zeta classical zero free region: There is an absolute c0>0 such that ζ has no zeros in σ1c0/log(t+2). The pole at s=1 is not a zero.

[F3]

Zeta reciprocal zero sum bound: For T2, the sum of 1/ρ over nontrivial zeros with 0<ImρT is O(log2T), with multiplicity. Adjoining any real nontrivial zeros preserves the estimate.

[F4]

The half-weighted Chebyshev function: For x>0, define ψ0(x)=n<xΛ(n)+{Λ(x)/2,xZ>0,0,xZ>0. This differs at prime powers from the right-continuous ψ(x)=nxΛ(n) of def-chebyshev-psi-function.

Proof

1.1

For each zero in the finite sum Imρ<T, the region implies xρxexp(c0logx/log(T+2)). Summing absolute values and using the reciprocal estimate, including any real zeros, bounds the entire zero sum by the first displayed error.

F2F3
2.1

The supplied truncation error is at most O(xlog2(xT)/T+logx) because its minimum is at most one. The fixed constant ζ(0)/ζ(0) and log(1x2) are bounded for x2. Finally ψ(x)ψ0(x)(logx)/2, so replacing the half-weighted value gives the asserted error, including prime-power endpoints. The supplied formula holds for all x,T at these bounds; if a contour construction avoids ordinates, a non-ordinate in [T,T+1] has comparable bounds.

F1F4step 1.1
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Chebyshev psi prime number theorem error

Statement

There is an absolute c>0 such that for x2, ψ(x)=x+O(xeclogx).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Zeta explicit formula zero free error balance: For x2 and finite T3, the classical region and truncated explicit formula give ψ(x)x=O(xec0logx/log(T+2)log2T+xlog2(xT)T+logx). Constants may be enlarged and the positive region constant decreased. The zero sum used in the proof is finite.

[F2]

Zeta bounds in classical zero free region: There are 0<c2<c1<c0 and C>0 such that for t3 and σ1c1/log(t+2), ζ/ζ(σ+it)Clog(t+2)Clog2(t+2). In the narrower c2 region, 1/ζ(s)Clog(t+2). For t3 and 1c2/log(t+2)σ2, ζ/ζ(s)+1/(s1)=O(1),1/ζ(s)=O(s1), with removable interpretations at one.

Proof

1.1

Put u=logx and choose a fixed A>0. For sufficiently large x take T=eAu3. Then log(T+2)=Au+O(eAu), so the finite-zero term is O(xu2e(c0/A)u+o(1)), the truncation term is O(xu4eAu), and the remaining error is O(u2).

F1
2.1

Choose 0<c<min(A,c0/A). For any fixed k and positive epsilon, ukeϵu is bounded; thus each error above is O(xecu). Enlarging the constant over the initial compact x-range proves the assertion for all x2.

step 1.1algebra
3.1

The contour interpretation is consistent with the same bound: take σ1=1c1/log(T+2) with a sufficiently small region constant and σ0=1+1/logx. Throughout tT the left edge stays in the proved region. At high heights the derivative is O(logT); integrating 1/s gives a vertical contribution O(xσ1log2T), and horizontal edges give O(xlog2(xT)/T). At bounded height the pole-subtracted estimate bounds the derivative by O(1+1/s1); on the left edge its integral is O(loglog(T+2)). Only the pole at one is crossed. These edge bounds explain the scale used in the finite-zero proof.

F2step 1.1step 2.1
CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Chebyshev theta prime number theorem error

Statement

For some absolute c>0 and all x2, θ(x)=x+O(xeclogx).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Chebyshev psi prime number theorem error: There is an absolute c>0 such that for x2, ψ(x)=x+O(xeclogx).

[F2]

Psi and theta differ by at most a square-root term: There are positive constants K1,K2 such that for every real x2, 0ψ(x)θ(x)K1xlogx and, for all sufficiently large x, ψ(x)θ(x)K2x.

Proof

1.1

The comparison gives 0ψ(x)θ(x)Kxlogx. Thus θ(x)xψ(x)x+Kxlogx.

F2
2.1

The first term has the asserted bound. Writing u=logx, the ratio of the second to xecu is u2eu2/2+cu, bounded on ulog2. This proves the result after enlarging the constant.

F1step 1.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Logarithmic integral

Definition

For real x2, define Li(x)=2xdtlogt. In particular Li(2)=0. The integral never crosses the singularity at one.

LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Logarithmic integral asymptotic expansion

Statement

For each fixed integer m1, as x, Li(x)=j=0m1j!xlogj+1x+Om(xlogm+1x).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Logarithmic integral: For real x2, define Li(x)=2xdtlogt. In particular Li(2)=0. The integral never crosses the singularity at one.

Proof

1.1

Let Jk(x)=2x(logt)kdt. Integration by parts gives Jk=x/logkx2/logk2+kJk+1. Starting with Li=J1, apply this identity m times: the remainder is m!Jm+1 and the lower-end constant is j=0m12j!/logj+12.

F1algebra
2.1

For x4, split Jm+1 at x. Its first part is at most x/(log2)m+1 and its second at most 2m+1x/logm+1x. The first bound and the fixed lower-end constant are also Om(x/logm+1x). This proves the expansion for each fixed m, including m=1.

step 1.1algebra
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Prime number theorem logarithmic integral

Statement

For some absolute c>0 and every x2, π(x)=Li(x)+O(xeclogx).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Chebyshev theta prime number theorem error: For some absolute c>0 and all x2, θ(x)=x+O(xeclogx).

[F2]

Logarithmic integral: For real x2, define Li(x)=2xdtlogt. In particular Li(2)=0. The integral never crosses the singularity at one.

[F3]

Abel summation recovers the prime-counting function from theta: For every real x2, π(x)=θ(x)logx+2xθ(t)tlog2tdt.

Proof

1.1

Set E(t)=θ(t)t. The exact partial-summation identity gives π(x)=x/logx+2xdt/log2t+E(x)/logx+2xE(t)/(tlog2t)dt. Integration by parts in the definition of Li makes its main term Li(x)+2/log2.

F2F3
2.1

For x4 split the error integral at x. The initial part is O(x) because E(t)=O(t). The second is O(xe(c0/2)logx) using the theta error and logtlog2. The endpoint error has the same form. Decrease the positive exponent constant and absorb 2/log2 and the compact range 2x4.

F1step 1.1
CorollaryStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Prime number theorem

Statement

As x, π(x)x/logx,θ(x)x,ψ(x)x. These three asymptotic assertions are equivalent.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Prime number theorem logarithmic integral: For some absolute c>0 and every x2, π(x)=Li(x)+O(xeclogx).

[F2]

Logarithmic integral asymptotic expansion: For each fixed integer m1, as x, Li(x)=j=0m1j!xlogj+1x+Om(xlogm+1x).

[F3]

Abel summation recovers the prime-counting function from theta: For every real x2, π(x)=θ(x)logx+2xθ(t)tlog2tdt.

[F4]

Psi and theta differ by at most a square-root term: There are positive constants K1,K2 such that for every real x2, 0ψ(x)θ(x)K1xlogx and, for all sufficiently large x, ψ(x)θ(x)K2x.

Proof

1.1

The quantitative counting theorem and the first Li term give π(x)x/logx, since logxeclogx0.

F1F2
1.2

Independently, if θ(x)x, the exact Abel formula gives π(x)x/logx: its integral is O(x/log2x), by splitting at x and using θ(t)=O(t).

F3
2.1

Conversely summing logp=logxpxdt/t over the finitely many primes px gives θ(x)=π(x)logx2xπ(t)dt/t. If π(t)t/logt, the integral is O(x/logx)=o(x) by the same square-root split, so θ(x)x. Finally 0ψ(x)θ(x)=O(xlogx)=o(x), proving both directions between theta and psi. Combine these implications with the first step.

F4step 1.1step 1.2
CorollaryStatement: AI-generatedProof: AI-adaptedaudited 2026-09-07Open item page →

Nth prime asymptotic

Statement

If pn is the n-th prime, then pnnlogn as n.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Prime number theorem: As x, π(x)x/logx,θ(x)x,ψ(x)x. These three asymptotic assertions are equivalent.

Proof

1.1

The counting asymptotic implies infinitely many primes, so pn. At these points n=π(pn)=pn(1+o(1))/logpn. Taking logarithms gives logn=logpnloglogpn+o(1), hence logn/logpn1.

F1
2.1

Rearrange the same positive quantities to obtain pn/(nlogn)=(pn/(nlogpn))(logpn/logn)1. Each factor is positive for all sufficiently large n, so these limits also yield the usual two-sided epsilon bounds.

step 1.1algebra
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Newman damped contour estimates

Statement

Let f:[0,)C be locally integrable with fB, let g(z)=0f(t)eztdt for Rez>0, and gT(z)=0Tf(t)eztdt. For R>0,T0, set KR(z)=(1+z2/R2)/z. On the right and left semicircles C+,C of radius R, C+(ggT)eTzKR(z)dz2πBR,CgTeTzKR(z)dz2πBR. Integrals at the imaginary endpoints are interpreted as improper limits when needed.

Facts & Assumptions

Given: The data and hypotheses of the statement.

Proof

1.1

For u=Rez>0, ggTBeTu/u. For u<0, gTB(eTu1)/(u), including the zero value at T=0. These inequalities follow by integrating the absolute values on the respective tail and finite interval.

givenalgebra
2.1

On z=R, KR(z)=2Rez/R2, since 1/z=z/R2. Multiplication by eTz therefore bounds either integrand by 2B/R2. The semicircle length is πR, giving both estimates. The same uniform bound makes integrals on arcs tending to either endpoint Cauchy, so the improper endpoint interpretation exists.

step 1.1algebra
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Newman zagier tauberian theorem

Statement

Let f:[0,)C be bounded and locally Lebesgue integrable. If g(z)=0f(t)eztdt, initially defined for Rez>0, extends holomorphically to an open set containing {Rez0}, then limT0Tf(t)dt=g(0).

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Newman damped contour estimates: Let f:[0,)C be locally integrable with fB, let g(z)=0f(t)eztdt for Rez>0, and gT(z)=0Tf(t)eztdt. For R>0,T0, set KR(z)=(1+z2/R2)/z. On the right and left semicircles C+,C of radius R, C+(ggT)eTzKR(z)dz2πBR,CgTeTzKR(z)dz2πBR. Integrals at the imaginary endpoints are interpreted as improper limits when needed.

[F2]

The residue theorem for a null-homologous cycle: Let ΩC be open, let f be meromorphic on Ω with pole set S, and let Γ be admissible for the residue theorem in Ω. Then Γf(z)dz=2πiaSn(Γ,a)Res(f,a), where only finitely many terms are nonzero.

[F3]

Dominated convergence: Let f and (fn) be measurable complex-valued functions such that fnf almost everywhere and fng almost everywhere for a single nonnegative measurable function g with gdμ<+. Then fL1(μ), fnfdμ0, and hence fndμfdμ.

Proof

1.1

Choose a bound B0 for f and fix R>0. The finite transform gT is entire: on compact z-sets its difference quotients and derivatives are dominated by integrable constants times f(t) on [0,T]. Compactness of the imaginary segment permits 0<δ<R such that the closed region {zR,Rezδ} and a neighborhood are in the continuation domain. Its positively oriented boundary C has a right semicircle and a left path staying strictly left except at its two endpoints.

F3given
2.1

Apply the residue theorem to (ggT)eTzKR(z) on C. Its sole possible pole is zero, with residue g(0)gT(0). Split the contour into the right arc, the g left-path integral, and minus the gT left-path integral. Deform the last integral to the left semicircle: gTeTzKR(z) is holomorphic in the region between these two left paths, which does not contain zero.

F2step 1.1
3.1

After division by 2π, the right-arc and left-semicircle absolute contributions are each at most B/R. On the fixed left path the g integrand is bounded independently of T, since the path misses zero, and tends to zero except at the endpoints. Dominated convergence makes that integral tend to zero. This argument applies to every sequence of real T tending to infinity, hence to the full limit. Thus lim supTg(0)gT(0)2B/R.

F1F3step 2.1
4.1

The radius R can be arbitrarily large; for each radius only its own positive strip width is needed. Letting R tend to infinity gives gT(0)g(0), which is precisely convergence of the asserted improper integral. If B=0 the assertion is immediate from the same estimates.

step 3.1algebra
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Monotone chebyshev tauberian desmoothing

Statement

Let A:[1,)[0,) be nondecreasing and locally integrable, with A(x)=O(x), and let a0. If 1(A(x)ax)x2dx converges, then A(x)/xa.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Cauchy criterion for improper integrals: The integral af converges if and only if, for every ε>0, there is A>a such that Au<vuvf<ε. At a finite right singular endpoint b, replace the condition by bδ<u<v<b; at a finite left endpoint use a<u<v<a+δ; at use u<vA. In each case all displayed proper integrals must exist.

Proof

1.1

Fix λ>1. The Cauchy criterion makes both tail integrals over [x,λx] and [x/λ,x] tend to zero. Monotonicity gives o(1)A(x)x(1λ1)alogλ,o(1)A(x)x(λ1)alogλ. These inequalities hold for sufficiently large x that x/λ1.

F1given
2.1

Therefore lim supA(x)/xaλlogλ/(λ1) and lim infA(x)/xalogλ/(λ1). Let λ1; both constants tend to a. This also works when a=0 (and nonnegativity supplies a zero lower bound). No differentiation of A or continuity at its jumps was used.

step 1.1algebra
LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Dirichlet character chebyshev laplace transform

Statement

Fix a Dirichlet character χ modulo q1. Put Ψχ(x)=nxχ(n)Λ(n) and δχ=1 for the principal character, zero otherwise. The bounded, locally integrable function fχ(t)=etΨχ(et)δχ has Laplace transform gχ(s)=L(s+1,χ)(s+1)L(s+1,χ)δχs(Res>0). After the removable value at zero is filled in, this extends holomorphically to an open neighborhood of the closed right half-plane.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Euler product for Dirichlet L-functions: For every Dirichlet character χ and every s with Res>1, L(s,χ)=p11χ(p)ps, and this product is nonzero on Res>1.

[F2]

Dirichlet series from arithmetic functions admit the Abel-summation integral formula: Let θR, let (an)n1 be complex coefficients, and put A(x):=1nxan. If A(x)=O(xθ), then for every s with s>θ, n1anns=s1A(x)xs1dx. For every integer N1 one has the endpoint formula 1nNanns=A(N)Ns+s1NA(x)xs1dx.

[F3]

Chebyshev's theta function has linear lower and upper bounds: There exist positive constants c<C and a real number x0 such that cxθ(x)Cx for every real xx0.

[F4]

Psi and theta differ by at most a square-root term: There are positive constants K1,K2 such that for every real x2, 0ψ(x)θ(x)K1xlogx and, for all sufficiently large x, ψ(x)θ(x)K2x.

[F5]

Nonprincipal Dirichlet L-functions are nonzero at one: If χχ0 is a Dirichlet character, then L(1,χ)0.

[F6]

Nonprincipal Dirichlet L-functions do not vanish on Re s = 1 away from s = 1: If χχ0 is a Dirichlet character, then L(1+it,χ)0 for every real t0.

[F7]

Nonprincipal Dirichlet L-functions are holomorphic on Re s greater than 0: If χχ0 is a Dirichlet character, then the Dirichlet series L(s,χ)=n1χ(n)ns converges for every Res>0 and defines a holomorphic function there.

[F8]

The principal Dirichlet L-function factors through zeta: Let χ0 be the principal Dirichlet character modulo q. Then on Res>1, L(s,χ0)=ζ(s)pq(1ps). Consequently, the meromorphic continuation of L(s,χ0) has a simple pole at s=1 with residue pq(11p)=φ(q)q.

[F9]

The Riemann zeta function has no zeros on the closed half-plane Res1, except for its pole at 1: The meromorphic continuation of ζ has no zeros on the closed half-plane Res1. Its only singularity there is the simple pole at s=1.

Proof

1.1

The linear theta bound and prime-power comparison give ψ(x)=O(x), uniformly after enlarging the constant for bounded x. Since χ(n)1, Ψχ(x)ψ(x); thus fχ is bounded and locally integrable, with only finitely many jumps on each compact t-interval.

F3F4
1.2

For nonprincipal chi, holomorphy on Rew>0 and nonvanishing at w=1 and at every 1+it, t0, show that the logarithmic derivative is holomorphic near every point of that line; the Euler product covers its right side. For the principal character, L(w,χ0)=ζ(w)pq(1pw) continues meromorphically, with a simple pole at one and no zero on Rew1. The finite factors cannot vanish there because pw<1.

F5F6F7F8F9
2.1

The Euler logarithm is normally absolutely convergent on Rew>1; its differentiated series is dominated on each smaller half-plane by (logn)nσ. Differentiation gives L/L(w,χ)=χ(n)Λ(n)nw. Apply the summatory integral at w=s+1 and substitute x=et, obtaining the displayed formula with the factor s+1 intact.

F1F2step 1.1
3.1

At s=0 in the principal case write L/L(1+s)=1/s+h(s) with h holomorphic. Then gχ0(s)=1/(1+s)+h(s)/(1+s) is holomorphic. Elsewhere shrink the pointwise neighborhoods to avoid s=-1. The union of these neighborhoods and the original half-plane is the required open set. For q=1 the finite product is empty and equals one.

step 2.1step 1.2algebra
TheoremStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-5.6-terra)audited 2026-09-07Open item page →

Prime number theorem arithmetic progressions

Statement

For every fixed integer q1 and integer a with gcd(a,q)=1, define ψ(x;q,a), θ(x;q,a) and π(x;q,a) by restricting their defining sums to integers, respectively primes, congruent to a modulo q. Then ψ(x;q,a)xφ(q),θ(x;q,a)xφ(q),π(x;q,a)Li(x)φ(q). No uniformity in a growing modulus is asserted.

Facts & Assumptions

Given: The data and hypotheses of the statement.

[F1]

Dirichlet character chebyshev laplace transform: Fix a Dirichlet character χ modulo q1. Put Ψχ(x)=nxχ(n)Λ(n) and δχ=1 for the principal character, zero otherwise. The bounded, locally integrable function fχ(t)=etΨχ(et)δχ has Laplace transform gχ(s)=L(s+1,χ)(s+1)L(s+1,χ)δχs(Res>0). After the removable value at zero is filled in, this extends holomorphically to an open neighborhood of the closed right half-plane.

[F2]

Newman zagier tauberian theorem: Let f:[0,)C be bounded and locally Lebesgue integrable. If g(z)=0f(t)eztdt, initially defined for Rez>0, extends holomorphically to an open set containing {Rez0}, then limT0Tf(t)dt=g(0).

[F3]

Orthogonality relations for Dirichlet characters modulo q: Let G=(Z/qZ)×, and let the sum range over all Dirichlet characters modulo q. 1. For unit classes a,bG, χmodqχ(a)χ(b)={φ(q),a=b,0,ab. 2. For Dirichlet characters χ,ψ modulo q, aGχ(a)ψ(a)={φ(q),χ=ψ,0,χψ.

[F4]

Monotone chebyshev tauberian desmoothing: Let A:[1,)[0,) be nondecreasing and locally integrable, with A(x)=O(x), and let a0. If 1(A(x)ax)x2dx converges, then A(x)/xa.

[F5]

Psi and theta differ by at most a square-root term: There are positive constants K1,K2 such that for every real x2, 0ψ(x)θ(x)K1xlogx and, for all sufficiently large x, ψ(x)θ(x)K2x.

[F6]

Abel summation recovers the prime-counting function from theta: For every real x2, π(x)=θ(x)logx+2xθ(t)tlog2tdt.

[F7]

Logarithmic integral asymptotic expansion: For each fixed integer m1, as x, Li(x)=j=0m1j!xlogj+1x+Om(xlogm+1x).

Proof

1.1

For each of the finitely many characters, the transform lemma and Newman theorem show convergence of 1(Ψχ(x)δχx)x2dx. This uses the change of variable x=et in the convergent truncated integrals.

F1F2
2.1

Orthogonality gives ψ(x;q,a)=φ(q)1χχ(a)Ψχ(x). For nonunits every character term is zero and, as a is a unit, so is the residue-class indicator. Thus finite summation of the preceding convergent integrals yields convergence for ψ(x;q,a)x/φ(q). This residue-class psi is nonnegative, nondecreasing and O(x), so desmoothing proves its asymptotic. No monotonicity of complex character sums was assumed.

F3F4step 1.1
3.1

The difference between class psi and class theta is nonnegative and bounded by the global prime-power difference, hence is o(x). Therefore class theta has the same main coefficient b=1/φ(q).

F5step 2.1
4.1

The Abel identity for this finite prime sum follows directly by summing 1=logp/logx+logppxdt/(tlog2t) over its primes. Hence class pi is class theta divided by log x plus its Abel integral. With θ(t;q,a)=bt+o(t), that integral is O(x/log2x) by splitting at square root x, so π(x;q,a)bx/logxbLi(x). The argument includes q=1 and allows constants to depend on q.

F6F7step 3.1

5 · Examples, counterexamples and false statements

None yet.

Sources