Formalization of the prime number theorem and Dirichlet's theorem

Abstract

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 asserts that the number $\pi (x)$ of primes less than $x$ is asymptotic to $x/\log x$, within the proof system Metamath.

4 pages, 1 figure, published at CICM 2016, FMM track

Cited by in corpus (1)

• A formal proof of Hensel's lemma over the p-adic integers