Basel problem

Statement

The series $\sum_{n=1}^{\infty} \frac{1}{n^2}$ converges, and $$\sum_{n=1}^{\infty} \frac{1}{n^2} = 1 + \frac{1}{4} + \frac{1}{9} + \cdots = \frac{\pi^2}{6}.$$

Remarks

The convergence follows from the p-series test with $p = 2$. The value is the hard part. The value $\pi^2/6 \approx 1.6449$ is $\zeta(2)$, where $\zeta$ is the Riemann zeta function. Mathlib states it as hasSum_zeta_two.

History

Pietro Mengoli posed the problem in 1650. Leonhard Euler solved it in 1734. The problem is named after Basel, the home town of Euler.

Explanations

L1 human

The sum of the reciprocals of the squares $1, 4, 9, 16, \dots$ is a finite number. Surprisingly, this number involves $\pi$, which comes from circles.