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

Tonelli and the geometric series compute int_0^1 int_0^1 1/(1-xy) dx dy = pi^2/6

Example

One has $\int_{0}^{1} \int_{0}^{1} \frac{1}{1 - x y} d x d y = \frac{π^{2}}{6} .$

Facts & Assumptions

Given: The function $(x, y) \mapsto (1 - x y)^{- 1}$ on $(0, 1)^{2}$ .

[L1]

For $0 \leq r < 1$ , the geometric series sums to $(1 - r)^{- 1}$ . (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges)

[L2]

Tonelli allows termwise summation of a nonnegative double series. (Tonelli's theorem for double series of nonnegative extended real numbers)

[A1]

The classical Basel identity is $\sum_{n \geq 1} \frac{1}{n^{2}} = \frac{π^{2}}{6} .$

Verification

technique · direct

1.1L1

For $(x, y) \in (0, 1)^{2}$ , [L1] gives $\frac{1}{1 - x y} = \sum_{n = 0}^{\infty} (x y)^{n}$ with nonnegative terms.

2.1L2step 1.1

Tonelli and [L2] allow termwise integration: $\int_{0}^{1} \int_{0}^{1} \frac{1}{1 - x y} d x d y = \sum_{n = 0}^{\infty} (\int_{0}^{1} x^{n} d x) (\int_{0}^{1} y^{n} d y) = \sum_{n = 0}^{\infty} \frac{1}{(n + 1)^{2}} .$

3.1A1step 2.1∎

Reindexing and applying [A1] yields $\int_{0}^{1} \int_{0}^{1} \frac{1}{1 - x y} d x d y = \sum_{m = 1}^{\infty} \frac{1}{m^{2}} = \frac{π^{2}}{6} .$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Gerald B. Folland, Real Analysis, 2nd ed., Exercise 55(b) (standard reference, not scraped)