Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24
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.

Γ(1/2)=π by Wallis's product

Statement

Γ(1/2)=π.

Facts & Assumptions

Given: Positive integers n tending to infinity.

[F1]

For x>0 and 0≤s≤1, x1−s≤Γ(x+1)/Γ(x+s)≤(x+1)1−s (Gautschi's inequality for the real Gamma function).

[F2]

If an=(2nn)/4n, then πn an→1 (The central binomial coefficient is asymptotic to 4^n divided by the square root of pi n).

[F4]

For every s>0, Γ(s+1)=sΓ(s) (The real Gamma functional equation Γ(s+1)=sΓ(s)).

Proof

technique · direct
1.1F4algebra

Iterating [F4] gives Γ(n+1/2)=Γ(1/2)∏k=0n−1(k+1/2)=((2n)!/(4nn!))Γ(1/2), with the empty product valid at n=0.

1.2F1

Apply [F1] with x=n and s=1/2. After inversion, n/(n+1)≤n Γ(n+1/2)/n!≤1, so this middle sequence tends to 1.

2.1step 1.1step 1.2F2F3algebra

By step 1.1 and [F3], the middle sequence is Γ(1/2)n(2nn)/4n. Fact [F2] makes its limit Γ(1/2)/π, while step 1.2 makes the same limit 1.

3.1step 2.1∎

Positivity of Gamma and uniqueness of limits therefore give Γ(1/2)=π.

Remarks

This proof uses Gautschi and Wallis. The Gaussian-integral proof Γ(1/2)=π from the Gaussian integral is logically independent of it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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