Formalization of the prime number theorem and Dirichlet's theorem

TL;DR

This paper formalizes key theorems in number theory, including Dirichlet's theorem and the prime number theorem, within the Metamath proof system, ensuring rigorous mathematical verification.

Contribution

It provides the first formal proof of Dirichlet's theorem and Selberg's proof of the prime number theorem in Metamath, advancing formal verification in number theory.

Findings

Formal proof of Dirichlet's theorem in Metamath

Formal proof of the prime number theorem in Metamath

Verification of classical number theory results within a proof system

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.