6 Explicit estimates

We will try to systematically collect explicit estimates related to the prime number theorem from the literature, and formalize them in a modular fashion. We divide such estimates into three classes:

• Primary explicit estimates: those that are directly control \(\psi (x)\) and \(M(x)\), usually via information on the zeta function.

• Secondary explicit estimates: these are useful general-purpose estimates on functions relating to the primes, such as bounds on the \(n\)-th prime, or estimates for the prime counting function \(\pi (x)\). These are generally derived from primary estimates and elementary arguments.

• Tertiary explicit estimates: these are bespoke applications to particular problems in analytic number theory or combinatorics that often require secondary estimates as input.

In this project we will state the best available primary estimates known in the literature, and try to formalize at least some of them; state the best available secondary estimates known in the literature, as well as various tools from passing from primary to secondary estimates, and formalize these; and then finally formalize some tertiary estimates as applications of the secondary ones.