Session-authored (Fable 5 assisted)

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.

✓ 12 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 10 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

pi: the Equivalent Characterizations

1 · Prerequisites

2 · Summary

Pi as twice the smallest positive zero of cosine defines $π$ as twice the least positive zero of cosine, while Pi is the first positive zero of sine and The zero sets of sine and cosine and the least positive common period 2 pi determine its sine-zero and periodicity properties. The polygonal definition of path length, its refinement monotonicity, and the speed-integral theorem from Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability provide the geometric background.

Circular length and a local Riemann-area convention lead to the circumference, regular-polygon, and disc-area characterizations of $π$ . Finite integral identities then give the Gregory-Leibniz series, the Wallis product and its central-binomial consequence, and Viète's cosine and nested-radical product. The concluding equivalence theorem collects the zero, period, geometric, series, and product formulas without changing the original definition.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Circular arcs, circumference as arc length, and diameter

Definition

Let $c = (c_{1}, c_{2}) \in R^{2}$ and $r > 0$ . A circular arc of the circle with centre $c$ and radius $r$ is a restriction

$γ_{c, r} ∣_{[α, β]}, γ_{c, r} (t) = c + r (\cos t, \sin t), α < β,$

taken as a parametrized path rather than as its image; its trace is that image. The parameter interval is part of the arc, because a set of points does not determine a length: the same trace is swept by restrictions of different lengths.

The arc's length is the path length of Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability computed with the Euclidean norm of The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ . The circumference $C (r)$ is $L (γ_{c, r})$ for the once-around parameter interval $[0, 2 π]$ , where $π$ is the constant of Pi as twice the smallest positive zero of cosine. Translation does not affect the value, so the notation suppresses $c$ . The diameter is $d (r) : = 2 r$ .

The phrase once around is part of the convention: a parametrized path that repeats the same trace can have a larger length.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Riemann area between two continuous graphs and the disc as a vertically simple region

Definition

Let $a < b$ , and let $g, f : [a, b] \to R$ be continuous with $g (x) \leq f (x)$ for every $x$ . The Riemann area between their graphs is

$area {(x, y) : a \leq x \leq b, g (x) \leq y \leq f (x)} : = \int_{a}^{b} (f (x) - g (x)) d x .$

The integral exists by A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion and is the Darboux integral of The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ . The square map is continuous by Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function and strictly increasing on the nonnegative reals by Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , so Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ makes its inverse square-root function continuous; existence and uniqueness are Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ . Hence, for $r > 0$ , the functions $x \mapsto \pm \sqrt{r^{2} - x^{2}}$ are well defined and continuous on $[- r, r]$ , and the closed disc of radius $r$ is the region between them.

This is a local convention for regions between continuous graphs. It does not assign an area to an arbitrary bounded planar set.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period

Statement

For a positive real $p$ , the following are equivalent:

$p = π$ ;
$p$ is the least positive zero of sine;
$p / 2$ is the least positive zero of cosine;
$2 p$ is the least positive common period of sine and cosine.

Facts & Assumptions

Given: A positive real $p$ .

[L1]

If $γ$ is the unique least positive zero of cosine, then $π = 2 γ$ (Pi as twice the smallest positive zero of cosine).

[L2]

$\sin π = 0$ , and $\sin x > 0$ for every $0 < x < π$ ; thus $π$ is the first positive zero of sine (Pi is the first positive zero of sine).

[L3]

Both sine and cosine have period $2 π$ , and no smaller positive number is a common period (The zero sets of sine and cosine and the least positive common period 2 pi).

Proof

technique · direct

1.1

If $p = π$ , then [L2] says that $p$ is the least positive zero of sine.

givenL2

1.2

If $p = π$ , write $π = 2 γ$ as in [L1]. Then $p / 2 = γ$ , the least positive zero of cosine.

givenL1algebra

1.3

If $p = π$ , then $2 p = 2 π$ , which is the least positive common period by [L3].

givenL3algebra

1.4

Conversely, if $p$ is the least positive zero of sine, then $p = π$ because [L2] identifies $π$ as that least positive zero.

givenL2

1.5

If $p / 2$ is the least positive zero of cosine, then [L1] gives $p / 2 = π / 2$ , hence $p = π$ .

givenL1algebra

1.6

If $2 p$ is the least positive common period, then [L3] gives $2 p = 2 π$ , hence $p = π$ .

givenL3algebra

2.1

Steps 1.1 to 1.6 prove every implication to and from $p = π$ , so the four conditions are equivalent.

step 1.1step 1.2step 1.3step 1.4step 1.5step 1.6∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The arc length of a unit semicircle is pi

Statement

Every once-traversed semicircle of radius $1$ has arc length $π$ . In particular, the upper unit semicircle $γ (t) = (\cos t, \sin t)$ , $0 \leq t \leq π$ , has length $π$ .

Facts & Assumptions

Given: The path $γ (t) = (\cos t, \sin t)$ on $[0, π]$ .

[L1]

Vector differentiation is componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L2]

The functions sine and cosine are differentiable, with $(\sin t)^{'} = \cos t$ and $(\cos t)^{'} = - \sin t$ (The derivatives of sine and cosine are cosine and minus sine).

[L3]

For every real $t$ , $\sin^{2} t + \cos^{2} t = 1$ (Parity and the Pythagorean identity for sine and cosine).

[L4]

A $C^{1}$ path has length equal to the integral of its Euclidean speed (If $γ : [a, b] \to R^{n}$ is continuous, differentiable on $(a, b)$ , and $γ^{'}$ extends continuously to $[a, b]$ , then $L (γ) = \int_{a}^{b} ∥ γ^{'} (t) ∥_{2} d t$ ).

[L5]

The integral of the constant function $1$ on $[a, b]$ is $b - a$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[L6]

Path length is invariant under every continuous surjective monotone reparametrization (Arc length is invariant under every continuous surjective monotone reparametrization, including pauses and reversal).

Proof

technique · direct

1.1

By [L1] and [L2], $γ^{'} (t) = (- \sin t, \cos t)$ on $[0, π]$ .

givenL1L2

2.1

By [L3], $∥ γ^{'} (t) ∥_{2} = \sqrt{\sin^{2} t + \cos^{2} t} = 1$ .

step 1.1L3algebra

3.1

By [L4] and [L5], $L (γ) = \int_{0}^{π} 1 d t = π$ .

step 2.1L4L5

4.1

Translating or rotating the displayed path does not change the differences between its points, and reversing or monotonically reparametrizing it does not change its length by [L6]. Thus every once-traversed unit semicircle has length $π$ .

step 3.1L6algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Every circle has circumference 2 pi r and circumference-to-diameter ratio pi

Statement

For every centre $c \in R^{2}$ and radius $r > 0$ , the once-traversed circle has circumference

$C (r) = 2 π r .$

Since its diameter is $d (r) = 2 r$ , one has $C (r) / d (r) = π$ .

Facts & Assumptions

Given: A centre $c \in R^{2}$ , a real $r > 0$ , and the once-around path $γ (t) = c + r (\cos t, \sin t)$ on $[0, 2 π]$ .

[L1]

Circumference is the length of this once-around path, and diameter is $d (r) = 2 r$ (Circular arcs, circumference as arc length, and diameter).

[L2]

Vector differentiation is componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral).

[L3]

$(\sin t)^{'} = \cos t$ , $(\cos t)^{'} = - \sin t$ , and $\sin^{2} t + \cos^{2} t = 1$ (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L4]

A $C^{1}$ path has length equal to the integral of its speed (If $γ : [a, b] \to R^{n}$ is continuous, differentiable on $(a, b)$ , and $γ^{'}$ extends continuously to $[a, b]$ , then $L (γ) = \int_{a}^{b} ∥ γ^{'} (t) ∥_{2} d t$ ).

[L5]

The integral of a constant $q$ on $[a, b]$ is $q (b - a)$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[L6]

Every once-traversed unit semicircle has length $π$ (The arc length of a unit semicircle is pi).

Proof

technique · direct

1.1

By [L2] and [L3], $γ^{'} (t) = r (- \sin t, \cos t)$ and $∥ γ^{'} (t) ∥_{2} = r$ , since $r > 0$ .

givenL2L3algebra

2.1

By [L1], [L4], and [L5], $C (r) = L (γ) = \int_{0}^{2 π} r d t = 2 π r$ .

step 1.1L1L4L5

3.1

Because $r > 0$ , the diameter $d (r) = 2 r$ is nonzero, and step 2.1 gives $C (r) / d (r) = (2 π r) / (2 r) = π$ .

givenstep 2.1L1algebra

4.1

At $r = 1$ , step 2.1 gives circumference $2 π$ , agreeing with the sum of the two semicircle lengths from [L6].

step 2.1L6algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi

Statement

For every natural $n \geq 3$ , let $I_{n}$ and $O_{n}$ be the perimeters of the regular $n$ -gons respectively inscribed in and circumscribed about the unit circle. Then

$I_{n} = 2 n \sin (π / n), O_{n} = 2 n \tan (π / n),$

$I_{n} < 2 π < O_{n} .$

The sequence $(I_{n})_{n \geq 3}$ is strictly increasing, $(O_{n})_{n \geq 3}$ is strictly decreasing, and both converge to $2 π$ , the circumference of the unit circle.

Facts & Assumptions

Given: A natural $n \geq 3$ , the regular inscribed and circumscribed $n$ -gons of the statement, and the functions $f (x) = \sin x / x$ and $g (x) = \tan x / x$ on $(0, π / 2)$ .

[L1]

The addition formulas hold for sine and cosine, and $\sin^{2} x + \cos^{2} x = 1$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L2]

Sine is strictly increasing on $[- π / 2, π / 2]$ , and cosine is strictly decreasing on $[0, π]$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[L3]

Tangent is $\sin x / \cos x$ and secant is $1 / \cos x$ on their natural domains; there $(\tan x)^{'} = \sec^{2} x$ and $(\sec x)^{'} = \sec x \tan x$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant).

[L4]

$(\sin x)^{'} = \cos x$ , $(\cos x)^{'} = - \sin x$ , $\sin 0 = 0$ , and $\cos 0 = 1$ ; sums, products, and quotients obey the usual derivative rules on their natural domains (The derivatives of sine and cosine are cosine and minus sine, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L5]

Differentiability implies continuity. On an interval, a continuous function with positive derivative at every interior point is strictly increasing, and one with negative derivative at every interior point is strictly decreasing (A function differentiable at $c$ is continuous at $c$ , On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed).

[L6]

$\lim_{x \to 0} \sin x / x = 1$ (The limit of sin x divided by x at zero is one).

[L7]

Sums, 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).

[L8]

The length of a path is the supremum of its polygonal lengths, and refinement cannot decrease polygonal length (Paths in $R^{n}$ , inscribed polygonal sums, arc length as their supremum, and rectifiability, Refining a partition cannot decrease its inscribed polygonal length).

[L9]

The unit-circle circumference is $2 π$ (Circular arcs, circumference as arc length, and diameter, Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).

[L10]

The Euclidean norm is induced by the sum of coordinate squares, and natural numbers in real formulas are the canonical naturals of the field (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L11]

The constant $π$ is positive and $π / 2$ is the least positive zero of cosine (Pi as twice the smallest positive zero of cosine).

[L12]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · direct

1.1

Since $n \geq 3$ and [L11] gives $π > 0$ , one has $0 < π / n < π / 2$ . By [L2] and [L4], both $\sin (π / n)$ and $\cos (π / n)$ are positive. Adjacent vertices of the inscribed polygon subtend angle $2 π / n$ ; using [L1] and [L10], their squared distance is $2 - 2 \cos (2 π / n) = 4 \sin^{2} (π / n)$ , so the side length is $2 \sin (π / n)$ and $I_{n} = 2 n \sin (π / n)$ .

givenL1L2L4L10L11algebra

1.2

By [L12], $π / n \to 0$ as $n \to \infty$ ; [L6] gives $f (π / n) \to 1$ . Also $\cos (π / n) \to 1$ by [L4] and [L5], so $g (π / n) = f (π / n) / \cos (π / n) \to 1$ by [L7].

L4L5L6L7L12

1.3

The derivative of $f$ has the sign of $x \cos x - \sin x$ . The function $h (x) = \sin x - x \cos x$ has derivative $x \sin x > 0$ on $(0, π / 2)$ by [L2] and [L4], and tends to $0$ at $0$ by [L4]. Hence $h (x) > 0$ , $f^{'} (x) < 0$ , and $f$ is strictly decreasing by [L5].

L2L4L5algebra

1.4

The derivative of $g$ has the sign of $k (x) = x \sec^{2} x - \tan x$ . From [L2] to [L4], $k^{'} (x) = 2 x \sec^{2} x \tan x > 0$ on $(0, π / 2)$ . Moreover, [L3], [L4], [L6], and [L7] give $k (x) \to 0$ as $x \to 0$ . Thus $g^{'} (x) > 0$ , so $g$ is strictly increasing by [L5].

L2L3L4L5L6L7algebra

2.1

The two tangent lines at adjacent vertices meet on the angle bisector. The resulting right triangle has adjacent side $1$ , opposite side half a polygon side, and angle $π / n$ ; by step 1.1 and [L3] its half-side is $\tan (π / n)$ , so $O_{n} = 2 n \tan (π / n)$ .

givenstep 1.1L3algebra

2.2

The inscribed edges form a polygonal approximation to the once-around circle, so [L8] and [L9] give $I_{n} \leq 2 π$ . By [L2] and [L4], $1 - \cos x > 0$ for $0 < x < π / 2$ ; hence [L4] and [L5] applied to $x - \sin x$ give $\sin x < x$ there and $I_{n} < 2 π$ .

step 1.1L2L4L5L8L9algebra

2.3

Since $n \mapsto π / n$ is strictly decreasing for $n \geq 3$ , step 1.3 gives $I_{n} = 2 π f (π / n) < 2 π f (π / (n + 1)) = I_{n + 1}$ .

step 1.1step 1.3algebra

3.1

The derivative of $\tan x - x$ is $\sec^{2} x - 1 = \tan^{2} x > 0$ on $(0, π / 2)$ by [L2] to [L5]. Thus $\tan x > x$ there, and step 2.1 gives $O_{n} > 2 π$ .

step 2.1L2L3L4L5algebra

3.2

Since $n \mapsto π / n$ decreases, step 1.4 gives $O_{n + 1} = 2 π g (π / (n + 1)) < 2 π g (π / n) = O_{n}$ .

step 2.1step 1.4algebra

4.1

Therefore $I_{n} = 2 π f (π / n) \to 2 π$ and $O_{n} = 2 π g (π / n) \to 2 π$ by [L7]. Together with [L9], the common limit is exactly the unit-circle circumference.

step 1.1step 2.1step 1.2L7L9∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi

Statement

For every $r > 0$ , the Riemann area of the closed disc of radius $r$ is $π r^{2}$ . In particular, the unit disc has area $π$ .

Facts & Assumptions

Given: A real $r > 0$ and the graph-area convention of Riemann area between two continuous graphs and the disc as a vertically simple region.

[L1]

If $φ$ is differentiable with integrable derivative and $f$ is continuous on an interval containing its image, then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ (Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ ).

[L2]

For every real $x$ , the quarter-turn shift formulas are $\sin (x + π / 2) = \cos x$ and $\cos (x + π / 2) = - \sin x$ , and in particular $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ . For all real $x, y$ , the sine and cosine addition formulas hold; moreover, $\sin^{2} x + \cos^{2} x = 1$ for every real $x$ (Quarter-turn values and shifts by pi/2 and pi, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L3]

$(\sin t)^{'} = \cos t$ and $(\cos t)^{'} = - \sin t$ (The derivatives of sine and cosine are cosine and minus sine).

[L4]

The Riemann integral is linear (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[L5]

If $G$ is differentiable at every point of $[a, b]$ , $f = G^{'}$ there, and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[L6]

The integral of the constant $1$ on $[a, b]$ is $b - a$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Proof

technique · direct

1.1

By the definition of graph area, the unit-disc area is $2 \int_{- 1}^{1} \sqrt{1 - x^{2}} d x$ .

given

1.2

For radius $r$ , the graph-area formula is $2 \int_{- r}^{r} \sqrt{r^{2} - x^{2}} d x$ . Substitute $x = r u$ by [L1]; since $r > 0$ , the integrand becomes $r \sqrt{1 - u^{2}}$ and $d x = r d u$ , so the value is $r^{2}$ times the unit-disc area.

givenL1algebra

2.1

Apply [L1] with $x = \sin t$ on $[- π / 2, π / 2]$ . Cosine is nonnegative there, so $\sqrt{1 - \sin^{2} t} = \cos t$ by [L2]; hence the area is $2 \int_{- π / 2}^{π / 2} \cos^{2} t d t$ .

step 1.1L1L2L3algebra

3.1

By [L2] and [L4], this equals $\int_{- π / 2}^{π / 2} 1 d t + \int_{- π / 2}^{π / 2} \cos (2 t) d t$ .

step 2.1L2L4algebra

4.1

The first integral is $π$ by [L6]. The second is $0$ : $(\frac{1}{2} \sin (2 t))^{'} = \cos (2 t)$ by [L3], and [L5] evaluates its endpoint difference as $0$ . Thus the unit-disc area is $π$ .

step 3.1L2L3L5L6algebra

5.1

Combining steps 4.1 and 1.2 gives area $π r^{2}$ for every $r > 0$ .

step 4.1step 1.2algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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

Statement

The series

$\sum_{k = 0}^{\infty} \frac{(- 1)^{k}}{2 k + 1}$

converges, and its sum is $π / 4$ . More precisely, for every natural $N$ ,

$\frac{π}{4} = \sum_{k = 0}^{N} \frac{(- 1)^{k}}{2 k + 1} + R_{N}, ∣ R_{N} ∣ \leq \frac{1}{2 N + 3},$

where

$R_{N} : = (- 1)^{N + 1} \int_{0}^{1} \frac{x^{2 N + 2}}{1 + x^{2}} d x .$

Facts & Assumptions

Given: A natural $N$ and the finite geometric identity used below.

[L1]

A series converges exactly when its sequence of finite partial sums converges (Series, partial sums, convergence and the sum, divergence, and the tail series).

[L2]

The Riemann integral is linear over finite sums (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[L3]

The power rule gives $(x^{m + 1})^{'} = (m + 1) x^{m}$ for $m \geq 0$ . If $G$ is differentiable on a closed interval and $f = G^{'}$ is integrable there, then $\int f$ is the endpoint increment of $G$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[L4]

If $m \leq f \leq M$ on $[a, b]$ , then the integral lies between $m (b - a)$ and $M (b - a)$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[L5]

Substitution holds for a differentiable inner map with integrable derivative and a continuous outer function (Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ ).

[L6]

On its natural domain, $\tan t = \sin t / \cos t$ , $\sec t = 1 / \cos t$ , and $(\tan t)^{'} = \sec^{2} t$ ; for every real $t$ , $\sin^{2} t + \cos^{2} t = 1$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, Derivatives and fundamental periods of tangent, cotangent, secant, and cosecant, Parity and the Pythagorean identity for sine and cosine).

[L7]

The quarter-turn values are $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ ; the sine and cosine addition formulas hold for all real inputs, sine is strictly increasing on $[- π / 2, π / 2]$ , cosine is strictly decreasing on $[0, π]$ , and $\sin 0 = 0$ , $\cos 0 = 1$ (Quarter-turn values and shifts by pi/2 and pi, The addition formulas for sine and cosine, Signs, monotonicity intervals, and ranges of sine and cosine, The derivatives of sine and cosine are cosine and minus sine).

[L8]

A sequence squeezed between two sequences with the same limit has that limit (The squeeze theorem).

[L9]

For every $ε > 0$ there is a natural $M \geq 1$ with $1 / M < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · direct

1.1

For every real $x$ , finite geometric algebra gives $\frac{1}{1 + x^{2}} = \sum_{k = 0}^{N} (- 1)^{k} x^{2 k} + (- 1)^{N + 1} \frac{x^{2 N + 2}}{1 + x^{2}} .$

givenalgebra

1.2

From [L7], the cosine double-angle formula at $π / 4$ gives $\cos^{2} (π / 4) = \sin^{2} (π / 4)$ , while the stated monotonicities make both values positive; hence [L6] gives $\tan (π / 4) = 1$ , and [L6] also gives $\tan 0 = 0$ . The definitions and Pythagorean identity in [L6] give $\sec^{2} t = 1 + \tan^{2} t$ . Apply [L5] with $x = \tan t$ on $[0, π / 4]$ . Then $d x = (1 + \tan^{2} t) d t$ , so $\int_{0}^{1} \frac{d x}{1 + x^{2}} = \int_{0}^{π / 4} 1 d t = \frac{π}{4} .$

L4L5L6L7algebra

2.1

Integrating step 1.1 on $[0, 1]$ and using [L2] and [L3] yields $\int_{0}^{1} \frac{d x}{1 + x^{2}} = \sum_{k = 0}^{N} \frac{(- 1)^{k}}{2 k + 1} + R_{N},$ where $R_{N} = (- 1)^{N + 1} \int_{0}^{1} x^{2 N + 2} / (1 + x^{2}) d x$ .

step 1.1L2L3

3.1

On $[0, 1]$ , $0 \leq x^{2 N + 2} / (1 + x^{2}) \leq x^{2 N + 2}$ , so [L3] and [L4] give $∣ R_{N} ∣ \leq 1 / (2 N + 3)$ .

step 2.1L3L4algebra

4.1

Steps 2.1 and 1.2 give the displayed finite-remainder identity. By [L9], $1 / (2 N + 3) \to 0$ , so step 3.1 and [L8] make the finite sums converge to $π / 4$ ; by [L1], this is the sum of the series.

step 2.1step 3.1step 1.2L1L8L9∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Wallis integrals satisfy the two-step recurrence, closed forms, and the adjacent-integral squeeze

Statement

For $n \in N$ , put

$I_{n} : = \int_{0}^{π / 2} \sin^{n} t d t .$

Then $I_{0} = π / 2$ , $I_{1} = 1$ , and for every $n \geq 2$ ,

$I_{n} = \frac{n - 1}{n} I_{n - 2} .$

Consequently, for every $m \geq 0$ ,

$I_{2 m} = \frac{π}{2} \prod_{k = 1}^{m} \frac{2 k - 1}{2 k}, I_{2 m + 1} = \prod_{k = 1}^{m} \frac{2 k}{2 k + 1},$

where an empty product is $1$ . For $m \geq 1$ ,

$I_{2 m + 1} \leq I_{2 m} \leq I_{2 m - 1}, 1 \leq \frac{I_{2 m}}{I_{2 m + 1}} \leq \frac{2 m + 1}{2 m},$

and therefore $I_{2 m} / I_{2 m + 1} \to 1$ .

Facts & Assumptions

Given: The functions $t \mapsto \sin^{n} t$ on $[0, π / 2]$ and the integrals $I_{n}$ .

[L1]

Integration by parts gives $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ when the stated derivatives are integrable (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ).

[L2]

$(\sin t)^{'} = \cos t$ , $(\cos t)^{'} = - \sin t$ , $\sin 0 = 0$ , $\cos 0 = 1$ , and $\sin^{2} t + \cos^{2} t = 1$ (The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine).

[L3]

Sine is strictly increasing on $[- π / 2, π / 2]$ , has range $[- 1, 1]$ , and satisfies $\sin (π / 2) = 1$ and $\cos (π / 2) = 0$ (Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi).

[L4]

The integral is linear; the integral of a constant $c$ on $[a, b]$ is $c (b - a)$ ; and if $f \leq g$ pointwise on $[a, b]$ then $\int_{a}^{b} f \leq \int_{a}^{b} g$ (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L5]

A finite product in a monoid has empty product equal to the identity and satisfies 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).

[L6]

A sequence squeezed between two sequences with the same limit has that limit (The squeeze theorem).

[L7]

The constant $π$ is positive (Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1

By [L3] and [L4], $I_{0} = \int_{0}^{π / 2} 1 d t = π / 2$ , while [L2] gives $I_{1} = [- \cos t]_{0}^{π / 2} = 1$ .

L2L3L4algebra

1.2

Let $n \geq 2$ . Apply [L1] to $u = \sin^{n - 1} t$ and $v^{'} = \sin t$ . The endpoint term $[- \sin^{n - 1} t \cos t]_{0}^{π / 2}$ is $0$ , including the first legal case $n = 2$ , and [L2] gives $I_{n} = (n - 1) \int_{0}^{π / 2} \sin^{n - 2} t \cos^{2} t d t .$

givenL1L2L3algebra

1.3

For $m \geq 1$ , [L2] and [L3] give $0 \leq \sin^{2 m + 1} t \leq \sin^{2 m} t \leq \sin^{2 m - 1} t$ , so the integral bounds in [L4] yield $I_{2 m + 1} \leq I_{2 m} \leq I_{2 m - 1}$ .

L2L3L4

2.1

Substitute $\cos^{2} t = 1 - \sin^{2} t$ in step 1.2 and use [L4]: $I_{n} = (n - 1) (I_{n - 2} - I_{n})$ , hence $I_{n} = ((n - 1) / n) I_{n - 2}$ .

step 1.2L2L4algebra

3.1

Iterating step 2.1 separately from the base values of step 1.1 gives the displayed even and odd product formulas; when $m = 0$ , [L5] makes them exactly $I_{0} = π / 2$ and $I_{1} = 1$ .

step 1.1step 2.1L5algebra

4.1

All $I_{j}$ are positive by the product formulas in step 3.1: their base values are positive by [L7], and every displayed factor is positive. Dividing step 1.3 by $I_{2 m + 1}$ and using step 2.1 at $n = 2 m + 1$ gives $1 \leq \frac{I_{2 m}}{I_{2 m + 1}} \leq \frac{I_{2 m - 1}}{I_{2 m + 1}} = \frac{2 m + 1}{2 m} .$

step 2.1step 1.3step 3.1L7algebra

5.1

Both outer sequences in step 4.1 tend to $1$ , so [L6] gives $I_{2 m} / I_{2 m + 1} \to 1$ .

step 4.1L6∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n

Statement

For $n \geq 1$ , put $a_{n} : = (\binom{2 n}{n}) / 4^{n}$ . Then

$\sqrt{π n} a_{n} ⟶ 1.$

Equivalently,

$(\binom{2 n}{n}) \sim \frac{4^{n}}{\sqrt{π n}},$

where the asymptotic notation means that the ratio of the two sides tends to $1$ .

Facts & Assumptions

Given: A natural $n \geq 1$ and the positive real $a_{n} = (\binom{2 n}{n}) / 4^{n}$ .

[L1]

For $k \leq n$ , $(\binom{n}{k}) k! (n - k)! = n!$ , so the usual factorial quotient equals the binomial coefficient ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ).

[L2]

For $n \in N$ , $W_{n} = \prod_{k = 1}^{n} (2 k)^{2} / ((2 k - 1) (2 k + 1))$ , with $W_{0} = 1$ , and $W_{n} \to π / 2$ (Wallis's product: pi over two is the limit of the finite Wallis products).

[L3]

[L4]

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

[L5]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L6]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L7]

The constant $π$ is positive (Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1

By [L1] and [L3], $a_{n} = \frac{(2 n)!}{(n!)^{2} 4^{n}} = \prod_{k = 1}^{n} \frac{2 k - 1}{2 k} .$

givenL1L3algebra

2.1

Comparing step 1.1 with the factors in $W_{n}$ gives $W_{n} = \frac{1}{(2 n + 1) a_{n}^{2}} .$

step 1.1L2L3algebra

3.1

By [L2], [L4], and step 2.1, $((π / 2) (2 n + 1) a_{n}^{2}) \to 1$ . Also $2 n / (2 n + 1) \to 1$ by [L6], so $π n a_{n}^{2} = \frac{2 n}{2 n + 1} \cdot \frac{π}{2} (2 n + 1) a_{n}^{2} ⟶ 1.$

step 2.1L2L4L6algebra

4.1

Let $b_{n} : = \sqrt{π n} a_{n} \geq 0$ , which is defined by [L5] and [L7]. Then $b_{n}^{2} = π n a_{n}^{2} \to 1$ by step 3.1, and $∣ b_{n} - 1 ∣ = \frac{∣ b_{n}^{2} - 1 ∣}{b_{n} + 1} \leq ∣ b_{n}^{2} - 1 ∣,$ so $b_{n} \to 1$ .

step 3.1L5L7algebra

5.1

For every $n \geq 1$ , the ratio of $(\binom{2 n}{n})$ to $4^{n} / \sqrt{π n}$ is exactly $\sqrt{π n} a_{n}$ . Thus either displayed asymptotic formulation implies the other, by the definition of asymptotic equivalence.

givenstep 4.1algebra

6.1

At $n = 0$ , $a_{0} = 1$ but the comparison term $4^{n} / \sqrt{π n}$ is undefined. The theorem starts at $n = 1$ , where every denominator in steps 1.1 to 5.1 is positive, and steps 4.1 and 5.1 prove its two equivalent formulations.

givenstep 1.1step 2.1step 3.1step 4.1step 5.1L1L7∎

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The finite Viete cosine product and its positive nested-radical factors

Statement

For every real $x$ and natural $n$ ,

$\sin x = 2^{n} \sin (x / 2^{n}) \prod_{k = 1}^{n} \cos (x / 2^{k}),$

with the product equal to $1$ when $n = 0$ . At $x = π / 2$ , all factors are positive and

$\cos (π / 4) = \frac{\sqrt{2}}{2}, \cos (π / 8) = \frac{\sqrt{2 + \sqrt{2}}}{2},$

with each later factor obtained by placing the previous positive radical inside $\sqrt{2 + \cdot} / 2$ .

Facts & Assumptions

Given: A real $x$ and a natural $n$ .

[L1]

For all real $x, y$ , $\sin (x + y) = \sin x \cos y + \cos x \sin y$ and $\cos (x + y) = \cos x \cos y - \sin x \sin y$ ; moreover, $\sin^{2} x + \cos^{2} x = 1$ for every real $x$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L2]

$\sin (π / 2) = 1$ , and cosine is positive on $(0, π / 2)$ (Quarter-turn values and shifts by pi/2 and pi, Signs, monotonicity intervals, and ranges of sine and cosine).

[L3]

Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L4]

A finite product in a monoid has empty product equal to the identity and is extended by adjoining 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).

Proof

technique · induction

1.1

At $n = 0$ , the right side is $2^{0} \sin x$ times the empty product, hence equals $\sin x$ by [L4].

baseL4algebra

1.2

Assume the finite identity at $n$ . Put $x = y = u / 2$ in the sine addition formula of [L1] to obtain $\sin u = 2 \sin (u / 2) \cos (u / 2)$ . Apply this with $u = x / 2^{n}$ and adjoin the factor $\cos (x / 2^{n + 1})$ using [L4]; this gives the identity at $n + 1$ .

ihL1L4algebra

1.3

At $x = π / 2$ , every angle $π / 2^{k + 1}$ lies in $(0, π / 2)$ , so [L2] makes every factor positive. Put $x = y = u / 2$ in the cosine addition formula of [L1] and use the Pythagorean identity there to obtain $\cos u = 2 \cos^{2} (u / 2) - 1$ . Thus $\cos (u / 2) = \frac{\sqrt{2 + 2 \cos u}}{2},$ where [L3] selects the positive square root.

L1L2L3algebra

2.1

By induction, the finite identity holds for every natural $n$ .

step 1.1step 1.2

3.1

Starting with $\cos (π / 2) = 0$ in [L2] and iterating step 1.3 gives $\cos (π / 4) = \sqrt{2} / 2$ , $\cos (π / 8) = \sqrt{2 + \sqrt{2}} / 2$ , and all subsequent positive nested-radical factors stated above.

step 2.1step 1.3L2L3discharge-induction∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Viete's nested-radical product: two over pi is the limit of the finite cosine products

Statement

Let

$P_{n} : = \prod_{k = 1}^{n} \cos (π / 2^{k + 1}), P_{0} : = 1.$

Then $P_{n} \to 2 / π$ . Equivalently, substituting the positive half-angle radicals from The finite Viete cosine product and its positive nested-radical factors,

$\frac{2}{π} = \frac{\sqrt{2}}{2} \cdot \frac{\sqrt{2 + \sqrt{2}}}{2} \cdot \frac{\sqrt{2 + \sqrt{2 + \sqrt{2}}}}{2} \dots,$

where the infinite product means the limit of its finite products.

Facts & Assumptions

Given: The finite products $P_{n}$ .

[L1]

For every $x$ and natural $n$ , $\sin x = 2^{n} \sin (x / 2^{n}) \prod_{k = 1}^{n} \cos (x / 2^{k})$ , and at $x = π / 2$ the factors have the stated positive nested-radical forms (The finite Viete cosine product and its positive nested-radical factors).

[L2]

$\lim_{x \to 0} \sin x / x = 1$ (The limit of sin x divided by x at zero is one).

[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).

[L4]

A finite product in a monoid has empty product equal to the identity (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).

[L5]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ , and $π > 0$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1

Apply [L1] with $x = π / 2$ and replace its index $n$ by $n + 1$ : $1 = 2^{n + 1} \sin (π / 2^{n + 2}) P_{n + 1} .$

L1algebra

2.1

Put $y_{n} : = π / 2^{n + 2}$ . Then $y_{n} > 0$ by [L5]. Since $2^{n + 2} \geq n + 1$ , [L5] gives $0 < y_{n} \leq π / (n + 1) \to 0$ , while $2^{n + 1} y_{n} = π / 2$ . Thus step 1.1 becomes $1 = \frac{π}{2} \frac{\sin y_{n}}{y_{n}} P_{n + 1} .$

step 1.1L5algebra

3.1

Every factor of $P_{n + 1}$ is positive by [L1], so division is legitimate. By [L2] and [L3], step 2.1 gives $P_{n + 1} \to 2 / π$ , hence also $P_{n} \to 2 / π$ .

step 2.1L1L2L3

4.1

The case $n = 0$ is the finite empty product $P_{0} = 1$ by [L4]; it is not an extra factor in the limit. Substituting the radical factors from [L1] into step 3.1 gives the displayed Viète product.

step 3.1L1L4∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

The zero, period, arc-length, polygonal, area, circumference, series, and product characterizations all give the same pi

Statement

The constant $π$ defined as twice the least positive cosine zero is also:

the least positive sine zero;
half the least positive common period of sine and cosine;
the length of a unit semicircle;
half the common limit of regular inscribed and circumscribed unit-circle perimeters;
the Riemann area of the unit disc;
$C (r) / d (r)$ for every circle of radius $r > 0$ ;
four times the Gregory-Leibniz series sum;
twice the Wallis-product limit;
twice the reciprocal of the Viète-product limit.

Facts & Assumptions

Given: The constant $π$ of the statement.

[L1]

The zero and least-common-period conditions are equivalent characterizations of $π$ (Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period).

[L2]

A once-traversed unit semicircle has length $π$ (The arc length of a unit semicircle is pi).

[L3]

Every positive-radius circle has circumference $2 π r$ and circumference-to-diameter ratio $π$ (Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).

[L4]

Regular inscribed and circumscribed unit-circle perimeters both tend to $2 π$ (Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi).

[L5]

The unit disc has Riemann area $π$ (A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi).

[L6]

The Gregory-Leibniz series converges to $π / 4$ (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).

[L7]

The finite Wallis products converge to $π / 2$ (Wallis's product: pi over two is the limit of the finite Wallis products).

[L8]

The finite Viète products converge to $2 / π$ (Viete's nested-radical product: two over pi is the limit of the finite cosine products).

Proof

technique · direct

1.1

Claims 1 and 2 are [L1].

1.2

Claim 3 is [L2], and claim 6 is [L3].

L2L3

1.3

Claim 4 follows from [L4] by dividing the common limit $2 π$ by $2$ , and claim 5 is [L5].

L4L5algebra

1.4

Claim 7 follows from [L6] by multiplying by $4$ , and claim 8 follows from [L7] by multiplying by $2$ .

L6L7algebra

1.5

By [L8], the Viète-product limit is $2 / π > 0$ , so twice its reciprocal is $2 / (2 / π) = π$ , which is claim 9.

L8algebra

2.1

Every listed value is therefore equal to the originally defined constant $π$ ; no one of these equalities was used to define another.

step 1.1step 1.2step 1.3step 1.4step 1.5∎

5 · Examples, counterexamples and false statements

None yet.

Sources

Standard references

Recommended treatments; not extraction sources.