# Proof: The infinite sum from n=1 to infinity of 1/n^2 equals exactly pi^2/6

- **Generated**: 2026-03-28
- **Verdict**: PROVED
- **Audit trail**: [proof_audit.md](proof_audit.md) | [proof.py](proof.py)

## Key Findings

- Sympy's symbolic summation computes sum_{n=1}^{inf} 1/n^2 = pi^2/6 exactly, confirmed by simplification to zero difference (A1).
- High-precision numerical computation via mpmath confirms zeta(2) = pi^2/6 to 60 decimal places (A2).
- An independent derivation via Parseval's theorem on the Fourier series of f(x) = x yields sum = pi^2/6 through an entirely different mathematical pathway (A3).
- All three methods agree, providing overwhelming computational evidence for this exact identity.

## Claim Interpretation

**Natural language**: "The infinite sum from n=1 to infinity of 1/n^2 equals exactly pi^2/6."

**Formal interpretation**: The claim asserts that the series sum_{n=1}^{infinity} 1/n^2 converges to precisely pi^2/6. This is an exact mathematical identity (the Basel problem, solved by Euler in 1735), not an approximation. The operator is strict equality (==). The proof verifies this via three independent computational methods: symbolic algebra, arbitrary-precision numerics, and Fourier analysis.

## Evidence Summary

| ID | Fact | Verified |
|----|------|----------|
| A1 | Symbolic computation of sum_{n=1}^{inf} 1/n^2 via sympy | Computed: Exact symbolic match (sum = pi^2/6) |
| A2 | High-precision numerical verification via mpmath zeta(2) | Computed: Agreement to 60 decimal places |
| A3 | Independent verification via Parseval's theorem on f(x)=x | Computed: Independently derives sum = pi^2/6 |

## Proof Logic

The proof establishes the Basel identity through three mathematically independent approaches:

**Method 1 — Symbolic computation (A1):** Using sympy's symbolic summation engine, the series sum_{n=1}^{inf} 1/n^2 is evaluated directly. Sympy returns pi^2/6 as the exact closed-form result. The difference between the computed sum and pi^2/6 simplifies to exactly zero, confirming the identity symbolically.

**Method 2 — High-precision numerics (A2):** Using mpmath's arbitrary-precision arithmetic at 60 decimal places, both zeta(2) (which equals sum 1/n^2 by definition) and pi^2/6 are computed independently. The values agree to all 60 computed digits, with a residual difference of ~3 x 10^{-61} attributable only to floating-point truncation at the 60th digit. This rules out any "near-miss" where the values might be close but not equal.

**Method 3 — Parseval's theorem (A3):** An entirely independent derivation uses Fourier analysis. For f(x) = x on [-pi, pi], Parseval's theorem states that (1/pi) * integral_{-pi}^{pi} x^2 dx equals the sum of squared Fourier coefficients. The left side evaluates to 2*pi^2/3. The Fourier sine coefficients are b_n = (-1)^{n+1} * 2/n, so b_n^2 = 4/n^2, and the right side equals 4 * sum(1/n^2). Equating: 2*pi^2/3 = 4*S, giving S = pi^2/6 (A3, confirmed symbolically via sympy).

The three methods use fundamentally different algorithms — symbolic Bernoulli number evaluation, arbitrary-precision Euler-Maclaurin summation, and Fourier analysis — making shared bugs extremely unlikely (A1, A2, A3 all agree).

## Counter-Evidence Search

1. **Could the sum converge to a value near but not equal to pi^2/6?** Computed both values to 60 decimal places; they agree exactly. No near-miss is possible.

2. **Is there any known error in sympy's summation of 1/n^2?** Cross-checked against two independent implementations (mpmath zeta and Parseval derivation). All three agree.

3. **Does the series actually converge?** All terms are positive, so partial sums increase monotonically. Convergence follows from the integral test (integral of 1/x^2 from 1 to infinity = 1 < infinity). No oscillation is possible.

4. **Could there be a subtlety with the Parseval derivation?** f(x) = x is continuous and bounded on [-pi, pi], hence square-integrable. Parseval's theorem applies unconditionally. The Fourier coefficients were verified symbolically.

## Conclusion

**PROVED.** The infinite sum sum_{n=1}^{infinity} 1/n^2 equals exactly pi^2/6. This identity is confirmed by three independent computational methods: symbolic algebra (exact match), arbitrary-precision numerics (60-digit agreement), and an independent Fourier-analytic derivation via Parseval's theorem. No counter-evidence or edge cases were found.

---

Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v0.10.0 on 2026-03-28.