ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passaudited 2026-08-29

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 sine product recovers the Basel sum

Example

The sine product implies the Basel identity

$\sum_{n \geq 1} \frac{1}{n^{2}} = \frac{π^{2}}{6} .$

Facts & Assumptions

Given: The product formula for $\sin (π z)$ .

[F1]

The Weierstrass product for sine is $\frac{\sin (π z)}{π z} = \prod_{n \geq 1} (1 - \frac{z^{2}}{n^{2}})$ (The Weierstrass product for sine).

[F2]

The complex sine power series gives $\frac{\sin (π z)}{π z} = 1 - \frac{π^{2} z^{2}}{6} + O (z^{4})$ near $z = 0$ (The exponential definitions of complex sine, cosine, hyperbolic sine, and hyperbolic cosine equal their entire power series).

Verification

1.1

For each $N \geq 1$ , the partial product $P_{N} (z) : = \prod_{n = 1}^{N} (1 - z^{2} / n^{2})$ has quadratic expansion $P_{N} (z) = 1 - (\sum_{n = 1}^{N} 1 / n^{2}) z^{2} + z^{4} R_{N} (z)$ , because every term beyond the linear choice from a single factor contains at least two copies of $z^{2}$ .

givenalgebra

2.1

The series $\sum 1 / n^{2}$ converges, so on a fixed neighbourhood of $0$ the functions $R_{N}$ stay bounded and the quadratic coefficients converge. Passing to the locally uniform limit supplied by [F1] gives $\prod_{n \geq 1} (1 - z^{2} / n^{2}) = 1 - (\sum_{n \geq 1} 1 / n^{2}) z^{2} + O (z^{4})$ .

F1step 1.1algebra

3.1

Comparing the quadratic terms in step 2.1 with the expansion from [F2] yields $\sum_{n \geq 1} 1 / n^{2} = π^{2} / 6$ .

F2step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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

Elias M. Stein and Rami Shakarchi, Complex Analysis, Ch. 5 Infinite products (standard reference, not scraped)
Matthias Weber, Complex Analysis, Ch. 3 §3.4 (standard reference, not scraped)