Number theory · existing Mathlib declaration

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

The theorem at a glance

Basel Problem — reciprocal squares sum to π²/6

A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.

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.

Formal orientation

Statement map

This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is 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.

Complementary intuition

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.

The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.

Authoritative formal type

Exact Mathlib statement

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

Selected evidence declaration text

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

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

These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.

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.

Provenance

Origin and evidence stay separate

Existing declaration: hasSum_zeta_two in mathlib
Relationship: The checked artifact is the upstream declaration itself
Preferred checked artifact: artifact.library.mathlib.basel-problem.v001
Source handling: Verified upstream reference; no mirrored source package