Euler-faithful Basel proof in Lean 4

Stream: mathlib4

[Bob Jefferson]

For those interested in the intersection of historical mathematics and formal verification, I’ve just finished a Lean 4 formalization of an Euler-faithful proof of the Basel identity (∑_{n=1}^∞ 1/n² = π²/6). The aim is not the shortest proof, but a historically aligned route - product over the zeros of sin(πz) and coefficient comparison at z = 0. The broader point is that Euler’s 1735 argument, while informal, can serve as a literal blueprint for a fully rigorous proof when expressed with modern local analytic language.

Method sketch:

• Work with the normalized function sin(πz)/(πz).

• Prove two quadratic expansions at 0.

  • Sine side: from cubic control of sin z plus a normalization/0-patching step.

  • Product side: avoid expanding an infinite product directly; extract the quadratic coefficient via a punctured-neighbourhood linear asymptotic for the logarithmic derivative of the Euler product limit function.

• Technical core (Phase 2C): rewrite logDeriv as a tsum of rational terms, perform termwise “Euler cancellation,” and justify passing the limit through the sum via a Tannery-type dominated convergence theorem with uniform summable domination on a punctured neighbourhood.

• Conclude via a small quadratic coefficient uniqueness lemma (baselSum = π²/6).

A Zenodo archive is in preparation. I’m happy to share the link privately on request.

I’d particularly appreciate pointers to any prior formalizations that follow a comparable Euler/product + coefficient-comparison route (rather than Fourier/Parseval or other modern methods).

[Bob Jefferson]

A quick update on the Euler-faithful Basel formalization: the project is now fully cleaned, builds reproducibly under a pinned toolchain, and has been archived. Happy to share details if useful to anyone.