TheoremStatement: Literature-sourcedProof: 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.

Wallis's product: pi over two is the limit of the finite Wallis products

Statement

For $m \in N$ , define the finite Wallis product

$W_{m} : = \prod_{k = 1}^{m} \frac{(2 k)^{2}}{(2 k - 1) (2 k + 1)},$

with $W_{0} = 1$ . Then

$\lim_{m \to \infty} W_{m} = \frac{π}{2} .$

This limit is the meaning of Wallis's infinite product for $π / 2$ .

Facts & Assumptions

Given: The finite products $W_{m}$ and the Wallis integrals $I_{n}$ .

[L1]

The Wallis integrals have the displayed even and odd product forms, and $I_{2 m} / I_{2 m + 1} \to 1$ (Wallis integrals satisfy the two-step recurrence, closed forms, and the adjacent-integral squeeze).

[L2]

A finite product in a monoid has empty product equal to the identity and obeys the recursion that adjoins its last factor (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

[L3]

Products and quotients of convergent real sequences have the corresponding limits when the limiting denominator is nonzero (Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct

1.1

Substituting the two product formulas of [L1] and collecting matching factors gives $\frac{I_{2 m}}{I_{2 m + 1}} = \frac{π}{2} \prod_{k = 1}^{m} \frac{(2 k - 1) (2 k + 1)}{(2 k)^{2}} = \frac{π / 2}{W_{m}} .$

L1L2algebra

2.1

At $m = 0$ , step 1.1 reads $I_{0} / I_{1} = π / 2 = (π / 2) / 1$ , so the empty-product boundary agrees with the identity. At $m = 1$ , it reads $I_{2} / I_{3} = 3 π / 8 = (π / 2) / (4 / 3)$ , so the first nonempty product agrees as well. Both checks are separate from the limiting assertion.

step 1.1L1L2algebra

2.2

By [L1], the left side of step 1.1 tends to $1$ . Since every $W_{m}$ is positive, rearranging gives $W_{m} = (π / 2) / (I_{2 m} / I_{2 m + 1})$ , and [L3] yields $W_{m} \to π / 2$ .

step 1.1L1L3

3.1

Thus the finite products, not an undefined completed multiplication, converge to $π / 2$ .

step 2.2∎

Depends on

Used by

Dependency tree · two levels

37 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

D. Galvin, Primitives and techniques of integration, section 13.2 (standard reference, not scraped)