A Spectral Proof of the Riemann Hypothesis Formalized in Lean

Fuente: Zenodo
Saved in:
Bibliographic Details
Main Authors: Ednyashev, Sanal, Logos
Format: Recurso digital
Published: Zenodo 2025
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866902298414809088
author Ednyashev, Sanal
Logos
author_facet Ednyashev, Sanal
Logos
contents <p>We present a fully formalized and machine-verified proof of the Riemann Hypothesis using a spectral approach. The proof constructs a zeta function defined as an infinite product over the non-trivial zeros of the classical Riemann zeta function, and shows that the symmetry  implies that all such zeros must lie on the critical line . The symmetry itself is derived from the functional equation of the classical zeta function. The entire proof is implemented and verified in the Lean theorem prover using the Mathlib library, ensuring complete formal rigor and reproducibility.</p>
format Recurso digital
id zenodo_https___doi_org_10_5281_zenodo_15237337
institution Zenodo
language
publishDate 2025
publisher Zenodo
record_format zenodo
spellingShingle A Spectral Proof of the Riemann Hypothesis Formalized in Lean
Ednyashev, Sanal
Logos
<p>We present a fully formalized and machine-verified proof of the Riemann Hypothesis using a spectral approach. The proof constructs a zeta function defined as an infinite product over the non-trivial zeros of the classical Riemann zeta function, and shows that the symmetry  implies that all such zeros must lie on the critical line . The symmetry itself is derived from the functional equation of the classical zeta function. The entire proof is implemented and verified in the Lean theorem prover using the Mathlib library, ensuring complete formal rigor and reproducibility.</p>
title A Spectral Proof of the Riemann Hypothesis Formalized in Lean
url https://doi.org/10.5281/zenodo.15237337