The Zeta Resonator: A Machine That Proves the Riemann Hypothesis in Lean
A fully formalized, irreducible, Lean-verified proof of the Riemann Hypothesis — open-source, auditable, and built from first principles. Test it yourself.
An Invitation to Test Something New
This is a complete Lean 4.2 formalization of a spectral approach to the Riemann Hypothesis.
It’s not a traditional paper or a sketch — it’s a logic circuit, constructed from first principles, compiled in Lean, and open to scrutiny.
At the heart is an operator: the Zeta Resonator. It’s self-adjoint, defined on a rigorous domain, and its spectrum corresponds to the nontrivial zeros of the Riemann zeta function.
It derives the trace identity that produces the zeta function, encodes the functional equation through operator duality, and proves completeness, convergence, and regularity from the ground up.
This project is not being submitted for review — it is being shared for transparency and testing. I’m offering it to the community to verify, critique, or build upon.
What It Includes:
A fully compiling Lean proof built from irreducible logic units (atomic lemmas and theorems)
17 modular components (ZRC001–ZRC017), supported by 5 appendices (A–E)
Spectral geometry and trace-class operator theory formalized in Lean
Construction of the core operator from scratch (no use of known zeros)
Formal derivation of the trace identity from heat kernel methods
Why It’s Different:
This is not a traditional math write-up. It’s code.
It runs in Lean. It uses no sorry. Every lemma and theorem is traceable to basic logic, built without circularity. There are no assumptions of the Riemann Hypothesis.
The structure mirrors a circuit diagram — modular, auditable, and interactive.
Who Might Be Interested:
Formal methods researchers interested in high-complexity Lean projects
Mathematicians with curiosity about operator-based approaches to RH
Lean programmers who want to stress-test a complete system
Skeptics who want to break it and prove it wrong
Where To Find It (all time stamped via BTC/SHA256):
Opentimestamp: https://drive.google.com/file/d/15r4lqV9eGBA_od-DKUDCJbRpbbo6R2cr/view?usp=sharing
Lean File: https://drive.google.com/file/d/1LXtYmCVwtMEzn73glQPW_noQxbxoeyfb/view?usp=sharing
Diagram: Included in Appendix E
Lean Version: 4.2+
Dependencies: mathlib4
Build Status: Fully compiling, no ‘
sorry’[versions updated 1012 MST, 23APR2025]
A Humble Ask
This project isn’t being presented with certainty — only with structure.
If you have the background and curiosity to test it, please do. If you find something useful in it, share it. If you find something broken, that’s welcome too.
It exists now. It runs. And it’s yours to explore.
-Bridger Logan
🧡 Support this project
If this work helped you — or if you believe formal mathematics should remain open, independent, and public — you can support it here:
Bitcoin (SegWit address):bc1qewl9aashxwIrap7aa6egqryyenf4g72lle6lek
All donations go toward continued public research in formalized mathematics.