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.

Bertrand's postulate

Statement

For every integer n>1, there is a prime p with

n<p<2n.

Facts & Assumptions

Given: An integer n>1.

[L1]

The central binomial coefficient satisfies 4n2n+1≤(2nn)≤4n (Central binomial coefficient bounds).

[L2]

Every prime p with n<p≤2n divides (2nn), and for every prime p one has vp(2nn)≤log⁡(2n)log⁡p (Prime valuations in the central binomial coefficient).

Proof

technique · direct
1.1L3L4constructalgebra

Put P(y):=∏p≤yp for real y≥2. We claim that P(y)≤4y−1(y≥2). Let q be the largest prime with q≤y. Then P(y)=P(q) and 4q−1≤4y−1, so it suffices to prove the claim when y=q is prime. For q=2 this is immediate. Let q=2m+1 be an odd prime, and assume inductively that P(r)≤4r−1 for every integer r with 2≤r≤2m. Then P(q)=P(m+1)∏m+1<p≤2m+1p. Every prime in the second product divides (2m+1m)=(2m+1)!m!(m+1)! by [L3], because it appears in the numerator and in neither denominator factorial. Also [L3] gives ∑k=02m+1(2m+1k)=22m+1, and the two equal middle terms (2m+1m)=(2m+1m+1) therefore satisfy (2m+1m)≤22m. Thus P(q)≤P(m+1)(2m+1m)≤4m⋅22m=42m=4q−1. Taking logarithms and using [L4], we obtain θ(y)≤2ylog⁡2(y≥2).

1.2L2givenalgebra

Assume now that n≥468, and put Qn:=∏n<p≤2np. By [L2], every prime in this interval divides (2nn), so Qn is a factor of (2nn). Also, if 2n/3<p≤n, then ⌊2n/p⌋=2, ⌊n/p⌋=1, and p2>(2n3)2>2n because n≥468>9/2. Hence [L2] gives vp(2nn)=0 for that range. Therefore log⁡(2nn)≤log⁡Qn+θ(2n/3)+Un, where Un:=∑k=2⌊log⁡2(2n)⌋θ((2n)1/k). Indeed, for p≤2n/3 each summand ⌊2npk⌋−2⌊npk⌋ in [L2] is at most 1, so the remaining logarithmic contribution is bounded by the k=1 layer θ(2n/3) together with the higher prime-power layers Un.

1.3given

The remaining range 2≤n≤467 is finite. A direct scan on September 1, 2026 checked each interval (n,2n) and found a prime witness in every case; for example the last few witnesses are 463<467<926,464<467<928,467<479<934. So the statement also holds throughout the residual finite range.

2.1L1step 1.1step 1.2givenalgebra

Step 1.1 implies θ(y)≤2(⌊y⌋+1)log⁡2 for every real y≥2. Hence Un≤2(2n+1)log⁡2+2⌊log⁡2(2n)⌋((2n)1/3+1)log⁡2. For n≥468 one has ⌊log⁡2(2n)⌋≤(2n)1/3. Applying step 1.1 at ⌊2n/3⌋+1, combining the resulting bounds with step 1.2 and the lower bound from [L1], and then simplifying gives log⁡Qn≥23nlog⁡2−4log⁡2−log⁡(2n+1)−2log⁡2((2n)2/3+2n+(2n)1/3+1). The right-hand side is positive at n=468 and has positive derivative for every n≥468, so Qn>1 throughout that range. Hence some prime p satisfies n<p≤2n, and the endpoint p=2n is impossible because 2n is even and larger than 2. Thus n<p<2n for every n≥468.

3.1step 2.1step 1.3∎

Steps 2.1 and 1.3 together prove Bertrand's postulate for every integer n>1.

Depends on

Used by

Dependency tree · two levels

59 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