An Euler-Faithful Lean 4 Formalization of the Basel Problem

This archive contains version v1.0.0 of: An Euler-Faithful Lean 4 Formalization of the Basel Problem Author: Bob JeffersonORCID: https://orcid.org/0009-0003-1460-055X This repository provides a fully formalized proof in Lean 4 of the classical Basel identity: ∑_{n=1}^∞ 1 / n² = π² / 6. The development is organized in an Euler-faithful manner. Rather than following a modern Fourier or Parseval approach, the formalization reconstructs the structural argument underlying Euler’s original method by comparing two independent quadratic expansions of the normalized function sin(πz) / (πz). The proof proceeds in three conceptual strands: A series-side expansion derived from a controlled Taylor development of sin z. A product-side expansion obtained via Euler’s infinite product, logarithmic derivative decomposition, summability control, and punctured-neighbourhood asymptotics. A quadratic coefficient uniqueness argument identifying the coefficients of the two expansions inside Lean. The final theorem establishes both the complex and real forms of the Basel identity. Formal and Engineering Properties Fully type-checked in Lean 4. No sorry placeholders. No additional axioms beyond those already present in mathlib. Uses only standard mathlib components. Pinned Lean toolchain (specified in lean-toolchain). Clean reproducible build via lake build. Includes a release verification script (scripts/release-build.ps1). Includes a complete accompanying manuscript (PDF and LaTeX source). The file EulerBasel/Audit/_Audit.lean prints the final theorem statements and their axiom dependencies during build for transparency. All reported axioms (propext, Classical.choice, Quot.sound) are standard classical axioms already present in mathlib. Reproducibility From the repository root: lake build A successful build confirms that the formalization type-checks under the pinned Lean toolchain. No external services are required beyond the initial mathlib cache retrieval handled automatically by Lake. Archive Integrity SHA-256 (ZIP archive): 11AD3BFD896CB2C0FF57477B5249F5CEB1C08215C81655BE017C0CA1104AFE62 Citation If referencing this artifact, please cite the Zenodo DOI assigned to this version.