ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 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.

A table of pi(x), theta(x), and psi(x)

Example

For $x = 10, 20, 30$ one has

$\begin{array}{ccccc} x & π (x) & θ (x) & ψ (x) & ψ (x) - θ (x) \\ 10 & 4 & 5.347108 & 7.832014 & 2.484907 \\ 20 & 8 & 16.087604 & 19.265658 & 3.178054 \\ 30 & 10 & 22.590395 & 28.476499 & 5.886104 \end{array}$

and the jumps of $ψ$ up to $30$ occur exactly at the prime powers $2, 3, 4, 5, 7, 8, 9, 11, 13, 16, 17, 19, 23, 25, 27, 29$ .

Facts & Assumptions

Given: The cutoffs $x = 10, 20, 30$ .

[L1]

$π (x)$ counts primes, $θ (x)$ sums $\log p$ over primes, and $ψ (x)$ sums $Λ (n)$ over integers $n \leq x$ (The prime-counting function, Chebyshev's theta function, Chebyshev's psi function).

[L2]

The function $ψ$ is the sum of $\log p$ over prime powers $p^{k} \leq x$ (Prime-power expansion of Chebyshev's psi function).

[L3]

The difference $ψ (x) - θ (x)$ is carried entirely by prime powers $p^{k}$ with $k \geq 2$ (Psi and theta differ by at most a square-root term).

Verification

technique · direct

1.1

For $x = 10$ , the primes are $2, 3, 5, 7$ , so $π (10) = 4$ and $θ (10) = \log 2 + \log 3 + \log 5 + \log 7.$ By [L2], the prime powers at most $10$ are $2, 3, 4, 5, 7, 8, 9$ , so $ψ (10) = 3 \log 2 + 2 \log 3 + \log 5 + \log 7.$ These are exactly the first row entries in the displayed table.

L1L2givenalgebra

2.1

The same calculation at $x = 20$ and $x = 30$ gives the remaining table rows. Up to $30$ , the extra contribution in $ψ - θ$ comes exactly from $4, 8, 9, 16, 25, 27$ , which is the prime-power layer described in [L3].

L1L2L3step 1.1algebra

3.1

The table illustrates two qualitative points from the A page: $ψ$ and $θ$ stay close, but $ψ$ jumps at every prime power while $θ$ jumps only at the primes.

L3step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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)