Formalization of the prime number theorem and Dirichlet's theorem

2016/08/05 by Carneiro, Mario
#03B35 (Primary) #11A41 #11F66 (Secondary) #11N05 #F.4.1 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1608.02029

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 π(x) of primes less than x is asymptotic to x/log x, within the proof system Metamath.

Related

• An alternative proof of the Dirichlet prime number theorem
• A Simple Proof Of The Prime Number Theorem
• A formally verified proof of the prime number theorem
• The prime number theorem for primes in arithmetic progressions at large values
• There are infinitely many prime numbers in all arithmetic progressions with first term and difference coprime