Formalization of the prime number theorem and Dirichlet's theorem

Mario Carneiro

We present the formalization of Dirichlet's theorem on the infinitude of primes in arithmetic progressions, and Selberg's elementary proof of the prime number theorem, which assert…