Formalizing Weil's Explicit Formula and Positivity Criterion for the Riemann Hypothesis in Lean
- 1Independent researcher, New Taipei City, Taiwan
Abstract
We present a Lean formalization of Weil’s explicit formula and positivity criterion for the Riemann hypothesis on a specified class of complex-valued functions with finitely many exceptional points and exponential decay. The zero functional is an unconditional sum over distinct zeros of the completed xi-function, with analytic multiplicities included once. The arithmetic functional is defined independently through pole, prime-power, and compensated archimedean terms. We establish the necessary integrability and summability results and transfer the explicit formula along one smooth, compactly supported approximation sequence. Uniform weighted derivative bounds include jump contributions and require no convergence of derivatives. For the converse criterion, a polynomial–Gaussian construction realizes a negative witness in the original test class whenever an off-critical-line zero exists. A summable majorant is fixed before the Gaussian width is chosen, so that an explicit finite parameter makes the negative main term dominate the entire zero sum. Alignment with Mathlib’s original Riemann hypothesis and a final value-identity bridge yield an arithmetic-side positivity criterion. We give source correspondence and distinguish the scopes of Lean compilation, separate-implementation checking, and model-assisted review. The result formalizes a classical equivalence; it establishes neither universal positivity of the functional nor the Riemann hypothesis itself.
This record contains the preprint, Online Resource 1 (ESM_1.pdf), and the source and evidence collection (ESM_2.zip). Author-owned manuscript and documentation materials are licensed under CC BY 4.0. Author-owned original code is licensed under Apache-2.0. Third-party materials retain their original licenses and notices. The file-level scope is specified in LICENSE_SCOPE.txt and LICENSE_SCOPE.json. The source collection supports inspection and correspondence with the accepted artifacts; it is not presented as a newly tested turnkey build.
Related
- Explicit formula for the discrete Laplace transform of the Möbius function, related special functions, and a criterion for the Riemann hypothesis
- Explicit formula for the Rasmussen invariant of odd pretzel knots
- An explicit positive formula for the sorting difference in Lam–Pylyavskyy Conjecture 53
- Multiplicative Colombeau algebras and the Nyman--Beurling criterion for the Riemann hypothesis
- Optimal explicit-formula bounds for analytic ranks: the limiting radix kernel
BibTeX
@misc{lin2026formalizing,
title = {{Formalizing Weil's Explicit Formula and Positivity Criterion for the Riemann Hypothesis in Lean}},
author = {Chin-Ken Lin},
howpublished = {Zenodo},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23494393},
url = {https://zenodo.org/records/23494393},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Formalizing Weil's Explicit Formula and Positivity Criterion for the Riemann Hypothesis in Lean
AU - Chin-Ken Lin
PY - 2026
DA - 2026/10/20
PB - Zenodo
DO - 10.5281/zenodo.23494393
UR - https://zenodo.org/records/23494393
AB - We present a Lean formalization of Weil’s explicit formula and positivity criterion for the Riemann hypothesis on a specified class of complex-valued functions with finitely many exceptional points and exponential decay. The zero functional is an unconditional sum over distinct zeros of the completed xi-function, with analytic multiplicities included once. The arithmetic functional is defined independently through pole, prime-power, and compensated archimedean terms. We establish the necessary integrability and summability results and transfer the explicit formula along one smooth, compactly supported approximation sequence. Uniform weighted derivative bounds include jump contributions and require no convergence of derivatives. For the converse criterion, a polynomial–Gaussian construction realizes a negative witness in the original test class whenever an off-critical-line zero exists. A summable majorant is fixed before the Gaussian width is chosen, so that an explicit finite parameter makes the negative main term dominate the entire zero sum. Alignment with Mathlib’s original Riemann hypothesis and a final value-identity bridge yield an arithmetic-side positivity criterion. We give source correspondence and distinguish the scopes of Lean compilation, separate-implementation checking, and model-assisted review. The result formalizes a classical equivalence; it establishes neither universal positivity of the functional nor the Riemann hypothesis itself. This record contains the preprint, Online Resource 1 (ESM_1.pdf), and the source and evidence collection (ESM_2.zip). Author-owned manuscript and documentation materials are licensed under CC BY 4.0. Author-owned original code is licensed under Apache-2.0. Third-party materials retain their original licenses and notices. The file-level scope is specified in LICENSE_SCOPE.txt and LICENSE_SCOPE.json. The source collection supports inspection and correspondence with the accepted artifacts; it is not presented as a newly tested turnkey build.
ER -