- Formalizing the Riemann Hypothesis in the Lean Interactive Theorem Prover
- Project Year:
2020
- REU Student (s):
Brandon Gomes | Rutgers University-New Brunswick NJ
- Student 1 Institution:
Rutgers University-New Brunswick
- Project Mentor:
Alex Kontorovich
- Project Mentor Area:
Mathematics
- Project Abstract:
The Riemann Hypothesis is a famous unsolved problem in mathematics first studied by Bernhard Riemann in 1859 which is important for understanding the distribution of prime numbers. In recent years, the development of type theory and automated theorem proving has made possible a new level of rigour in the ability for computers to check mathematical proofs. In this project, we formalize the statement of the Riemann Hypothesis in the Lean Theorem Prover using elementary methods in analysis and study the minimal algebraic requirements necessary to construct the statement of the Riemann Hypothesis.
