ExampleConstruction: AI-generatedVerification: 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.

The residual finite-range check for Bertrand's postulate

Example

The proof of Bertrand's postulate above isolates a finite residual range: its asymptotic inequality closes all cases $n \geq 468$ , so only $2 \leq n \leq 467$ must be checked directly.

Facts & Assumptions

Given: The residual range $2 \leq n \leq 467$ from Bertrand's postulate.

[L1]

Bertrand's postulate is already proved abstractly, with the only explicit finite remainder being the interval $2 \leq n \leq 467$ (Bertrand's postulate).

Verification

technique · direct

1.1

The following short certificate covers the entire residual range. Each displayed number is prime, and a prime $p$ is a witness for every integer $n$ with $p / 2 < n < p$ : $\begin{array}{cc} p & integers n covered \\ 3 & 2 \\ 5 & 3 – 4 \\ 7 & 4 – 6 \\ 13 & 7 – 12 \\ 23 & 12 – 22 \\ 43 & 22 – 42 \\ 83 & 42 – 82 \\ 163 & 82 – 162 \\ 317 & 159 – 316 \\ 631 & 316 – 630 \end{array}$ Consecutive ranges in the second column overlap or meet consecutively, and their union contains every integer from $2$ through $467$ . For each covered $n$ , the corresponding prime satisfies $n < p < 2 n$ .

givenalgebra

2.1

Therefore the finite residual range required by [L1] is closed. This check is evidence for the remaining finitely many cases only; it does not replace the asymptotic part of the theorem.

L1step 1.1∎

Depends on

Bertrand's postulate

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Victor Shoup, A Computational Introduction to Number Theory and Algebra, Version 2 (standard reference, not scraped)