- Formalizing Elementary Analytic Number Theory in Lean
- Project Year:
2022
- REU Student (s):
Emma Hasson | Bard College at Simon's Rock MA
- Student 1 Institution:
Bard College at Simon's Rock
- Project Mentor:
Alex Kontorovich
- Project Mentor Area:
Mathematics
- Project Abstract:
We formalized essential theorems in Elementary Analytic Number Theory into the Lean 3 Theorem Prover, with the eventual goal of contributing the work to the already vast library or formalized math in Lean called Mathlib. We focused on Dirichlet's Hyperbola Method as applied to the Divisor function beginning with a mathematical description of the theorem.
