https://github.com/0xjepsen/lean-riemann-hypothesis
Riemann Hypothesis in Lean
Science Score: 10.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
○CITATION.cff file
-
○codemeta.json file
-
○.zenodo.json file
-
○DOI references
-
✓Academic publication links
Links to: zenodo.org -
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (5.0%) to scientific vocabulary
Last synced: 10 months ago
·
JSON representation
Repository
Riemann Hypothesis in Lean
Basic Info
- Host: GitHub
- Owner: 0xJepsen
- License: mit
- Default Branch: master
- Homepage: https://reu.dimacs.rutgers.edu/~bg441/
- Size: 1.77 MB
Statistics
- Stars: 0
- Watchers: 0
- Forks: 0
- Open Issues: 0
- Releases: 0
Fork of bhgomes/lean-riemann-hypothesis
Created over 2 years ago
· Last pushed over 5 years ago
https://github.com/0xJepsen/lean-riemann-hypothesis/blob/master/
# Riemann Hypothesis in Lean [](https://zenodo.org/badge/latestdoi/275204877) _by Brandon H. Gomes and Alex Kontorovich through the Department of Mathematics, Rutgers University_ ## Formalization The Riemann Hypothesis is formalized by assuming some algebraic properties of the real and complex numbers and the existence/properties of the complex exponential function and the real logarithm. These axioms are then used to construct the Dirichlet function which we use to define the Riemann Hypothesis as the following type: ```lean (Re s (0,1)) (eta s = 0) (Re s = 1/2) ``` We also include the file, [`mathlib/impl.lean`](src/mathlib/impl.lean), which is a witness that the axioms can be proved using [`mathlib`](https://github.com/leanprover-community/mathlib). ## Acknowledgements We would like to thank Alex Best, Kevin Buzzard, Colin Fan, Sebastien Gouezel, Heather Macbeth, and the Zulip Lean community for many suggestions that made this project possible. The work of the first-named author was supported by the Rutgers Math Department through the DIMACS REU, and both are supported in part by the second-named author's NSF grant DMS-1802119.
Owner
- Name: Jepsen ✨
- Login: 0xJepsen
- Kind: user
- Location: Somewhere in meatspace
- Website: https://www.networkspirits.com/
- Twitter: 0xjepsen
- Repositories: 12
- Profile: https://github.com/0xJepsen
Creating Biodigital Jazz