We present the formalization of Dirichlet's theorem on the in nitude 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.
N 2 N ^ A 2 Z ^ gcd(A; N ) = 1 ! fp 2 P j N j(p A)g
N
(x) x 2 (1; 1) 7! x= log x
These two theorems are interesting formalization targets as they both have simple statements and \deep" proofs, and they are also both members of the \Formalizing 100 theorems" list maintained by Freek Wiedijk [Wie16], which tracks formalizations of 100 of the most famous theorems in mathematics.
Both proofs were written concurrently, over the course of about seven weeks between April 7 and June 1, 2016. This was done mostly because both theorems are in the same general subject (elementary number theory) and required similar techniques (mostly asymptotic approximation of nite sums of reals). The primary informal text used for the proof was Shapiro [Sha83], which devotes a section to Dirichlet's theorem and the whole nal chapter to Selberg and Erd}os's proof of the prime number theorem. 2
The present work is only a broad overview of the problem and proof method. Interested readers are invited to consult the main theorems pnt and dirith at [Met16], where the exact proof is discussed in detail.
The main arithmetic functions used in the formalization are: (x) = jfp 2 P j p xgj =
X 1 p x (x) =
X log p p x (n) = (log p 0 9p 2 P; k > 0 : n = pk o:w: (x) = X
(n) n x
Additionally, the Mobius function (n) is a very useful tool in sum manipulations. It is the unique multiplicative function such that (1) = 1 and Pdjn (d) = 0 for n > 1. This yields the Mobius inversion formula: if f (n) = Pdjn g(d), then g(n) = Pdjn (d)f (d). Since j (n)j 1, this is a very powerful technique for estimating sums \by inversion".
The proof of Hadamard and Vallee-Poussin relies on some deep theorems in complex analysis, such as Cauchy's theorem, which were not available at the time of this formalization, so instead we targeted the \elementary" proof discovered half a century later semi-independently by Erd}os and Selberg. The key step in both proofs is the Selberg symmetry formula:
x: Theorem 4 (pntrlog2bnd).
uv x n x X n x (n) log n + X
(u) (v) = 2x log x + O(x): jR(x)j log2 x
2 X jR(x=n)j log n + O(x log x):
The goal is to show (x) loxg x , but it is easily shown that (x) (x) (x) log x, so it is equivalent to show that (x) x, or R(x)=x ! 0, to establish the PNT. Given an eventual bound jR(x)j ax and the estimation Pn x long n = 12 log2 x + O( loxg x ), an application of Theorem 4 reproduces the original estimate jR(x)j ax + o(x), but using improved bounds on R(x) on small intervals we can improve the estimate to jR(x)j (a ca3)x + o(x) for a xed constant c, which produces a sequence of eventual bounds approaching zero, which proves R(x)=x ! 0 as desired.
In Dirichlet's theorem, the focal point is instead the Dirichlet characters modN , which are group homomorphisms from (Z=N Z) to C , extended to Z=N Z with value 0 at non-units, but the general theme of estimation of sums involving ; ; log and the characters (n) is the same. 3
In keeping with Metamath's tradition of minimal complexity, we used a minimum of de nition. Asymptotic estimations are reduced to the class O(1) of eventually bounded functions, partial functions R ! C such that for some c; A, x c implies jf (x)j A. An equation such as f 2 O(g) is rewritten as f =g 2 O(1) (which is correct as long as g is eventually nonzero, which is always true in cases of interest), and similarly f 2 o(g) is rewritten as f =g 0.
A few nite summation theorems take us a long way; two number-theory speci c summation theorems are the following divisor sum commutations:
X X A(k; d) = X X A(dm; d) kjn djk
djn mjn=d X X A(n; d) = X X
A(dm; d) n x djn
d x m n=d
A small amount of calculus was used in the proof, mostly through the following sum estimation theorem, which for example evaluates Pn x long n = 12 log2 x + O( loxg x ): Theorem 5 (dvfsumrlim). If F is a di erentiable function with F 0 = f , and f is a positive decreasing function that converges to zero, then g(x) = Pn x f (n) F (x) converges to some L and jg(x) Lj f (x). 4
The comparison of parallel proof attempts in di erent systems is usually confounded by the many other factors, so these statistics should not be given undue credence. According to [Avi07], Avigad's PNT project was a year-long project by four people, with the majority of the work happening during one summer, while this was a solo project over about seven work weeks. Dirichlet's theorem is 10 pages of informal text of [Sha83], and the PNT is 37 pages. Although the number of lines in the current proofs seem competitive, this is lost in the gzipped version, because the stored Metamath proof is already largely compressed, while the Isabelle and HOL scripts are plain text.
The de Bruijn factors for this work had to be estimated because the TeX source for the informal text was not available, but indications suggest that it fares poorly with comparatively large factors 19.9 and 7.67, respectively. However, when reading these statistics it is important to realize that Metamath stores proofs, not proof scripts like Isabelle and HOL. Every inference in the proof is an axiom or theorem of the system, and no proof searches are conducted by the veri er. This is re ected in the incredibly small veri cation time, which is normal for Metamath proofs. We do not have exact data on veri cation time for HOL Light, but it is believed to be on the order of minutes to hours.
These proofs are important milestones for the Metamath project. They demonstrate that even the largest of formalization projects in high level languages can also be conducted in a \full transparency"-style system like Metamath, with entirely worked-out proofs and with all automation o oaded from the veri er to the proof generation. [Dir37] Dirichlet, P. G. L.: Beweis des Satzes, dass jede unbegrenzte arithmetische Progression, deren erstes Glied und Di erenz ganze Zahlen ohne gemeinschaftlichen Factor sind, unendlich viele Primzahlen enthalt. Abhand. Ak. Wiss. Berlin 48, 313{342 (1837) [Sha83] Shapiro, H.: Introduction to the theory of numbers. John Wiley & Sons Inc., New York (1983)