Existing in Mathlib · Number theory

Basel Problem

The sum of the reciprocals of the positive perfect squares is exactly π squared divided by six.

Basel problem
reciprocal-square series
Bernoulli functions
Fourier coefficients
even zeta values

Exact theorem

Exact Mathlib statement

theorem hasSum_zeta_two : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 2) (π ^ 2 / 6)

The theorem at a glance

Basel Problem — reciprocal squares sum to π²/6

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

A dark green and ivory theorem poster states the reciprocal-square identity and traces the checked route from Bernoulli functions through Fourier coefficients and the general even-power sum to exponent two. — Mathlib's exponent-two specialization turns the Bernoulli–Fourier evaluation into the exact reciprocal-square sum.

Statement structure

From hypotheses to conclusion

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Original pixels inspected. The distinct Scientific diagram labels the reciprocal-square area model, keeps a separate zero-contribution socket for the natural-index zero term, graphs B₂(x) = x² − x + 1/6 on 0 ≤ x ≤ 1, displays the exact cosine-series identity, and evaluates x = 0 through cos(0) = 1 and B₂(0) = 1/6 to the exact result π²/6. Its illustrated sample squares decrease in the labelled 1, 1/2, 1/3 order and continue into a nonfinite tail; the equations, rather than their illustrative pixel areas, carry the exact ratios. — The reciprocal-square coefficients converge through the Bernoulli–Fourier route to π²/6.

Why it matters

A mathematical landmark

The Basel problem is one of the most recognizable exact evaluations of an infinite series. Mathlib's declaration exposes it as a concise specialization resting on a substantial Bernoulli-function and Fourier-coefficient development.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This page presents Mathlib's real HasSum statement for n ↦ 1/(n:ℝ)^2 with value π^2/6. Its natural-number indexing includes n = 0, whose term is zero under Lean's totalized real division, so it represents the usual series over positive integers. The selected declaration is only the exponent-two specialization, not a generic theorem about all zeta values.

The exact declaration is a real HasSum statement indexed by natural numbers.
The n = 0 term is zero because real division in Lean is totalized; the nonzero terms form the usual positive-index series.
The selected declaration concerns exponent two only and is not itself the general even-zeta theorem.
It gives an exact sum, not a quantitative convergence rate or error bound.
ProofAtlas is indexing an existing Mathlib theorem, not claiming a new proof or new mathematics.
The generated explanation and visuals are not proof evidence.

Source and local evidence

Where the theorem comes from

Existing declaration: hasSum_zeta_two in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.basel-problem.v001
Source: Open the pinned upstream reference