ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-13

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.

Gregory-Leibniz partial sums bracket pi with an explicit remainder bound

Example

Set

$S_{N} : = \sum_{k = 0}^{N} \frac{(- 1)^{k}}{2 k + 1} .$

Then $4 S_{N}$ is an upper bound for $π$ when $N$ is even, a lower bound when $N$ is odd, and in every case

$∣ π - 4 S_{N} ∣ \leq \frac{4}{2 N + 3} .$

Facts & Assumptions

Given: A natural number $N$ and the partial sum $S_{N}$ .

[L1]

The finite-remainder identity gives $\frac{π}{4} = S_{N} + (- 1)^{N + 1} \int_{0}^{1} \frac{t^{2 N + 2}}{1 + t^{2}} d t,$ where the integral is nonnegative and at most $1 / (2 N + 3)$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

Verification

technique · direct

1.1

Multiplying [L1] by $4$ gives $∣ π - 4 S_{N} ∣ \leq 4 / (2 N + 3)$ .

L1algebra

1.2

If $N$ is even, the remainder in [L1] has negative sign, so $π \leq 4 S_{N}$ ; if $N$ is odd, it has positive sign, so $4 S_{N} \leq π$ .

L1cases

1.3

Direct summation gives $S_{0} = 1, S_{1} = \frac{2}{3}, S_{2} = \frac{13}{15}, S_{3} = \frac{76}{105} .$

givenalgebra

2.1

Hence the first certified brackets include $\frac{8}{3} < \frac{304}{105} \leq π \leq \frac{52}{15} < 4,$ with the weak inequalities adjacent to $π$ supplied by step 1.2.

step 1.2step 1.3algebra

3.1

The error bound decreases only on the scale $1 / N$ , so the certification also records the slow convergence of these partial sums.

step 1.1algebra∎

Depends on

The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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

J. Lebl, Basic Analysis II, Exercise 11.4.11 (standard reference, not scraped)