A formally verified proof of the prime number theorem

ABSTRACT

The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdös in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

REFERENCES

• 1: Apostol, T. M. 1976. Introduction to Analytic Number Theory. Springer-Verlag.
• 2: Avigad, J. 2003. Number theory and elementary arithmetic. Philosophia Mathematica 11, 257--284.
• 3: Avigad, J. 2004. Notes on a formalization of the prime number theorem. Tech. rep. CMU-PHIL-163, Carnegie Mellon University.
• 4: Avigad, J. and Donnelly, K. 2004. Formalizing O notation in Isabelle/HOL. In Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR), D. Basin and M. Rusinowitch, Eds. vol. 3097, Lecture Notes in Artificial Intelligence, Springer-Verlag, 357--371.
• 5: Avigad, J. and Friedman, H. 2006. Combining decision procedures for the reals. Logic. Meth. Comput. Sci. 2,(4:4), 1--42.
• 6: Cornaros, C. and Dimitracopoulos, C. 1994. The prime number theorem and fragments of PA. Arch. Math. Logic 33, 4, 265--281.
• 7: Edwards, H. M. 2001. Riemann's Zeta Function. Dover Publications Inc., Mineola, NY.
• 8: Hardy, G. H. and Wright, E. M. 1979. An Introduction to the Theory of Numbers, 5th Ed. Oxford University Press, New York.
• 9: Jameson, G. J. O. 2003. The Prime Number Theorem. London Mathematical Society Student Texts, vol. 53. Cambridge University Press, Cambridge, UK.
• 10: McLaughlin, S. and Harrison, J. 2005. A proof producing decision procedure for real arithmetic. In Proceedings of the Automated Deduction---CADE-20. 20th International Conference on Automated Deduction (CADE '20). Tallinn, Estonia, R. Nieuwenhuis, Ed. Lecture Notes in Artificial Intelligence, vol. 3632, 295--314.
• 11: Nathanson, M. B. 2000. Elementary Methods in Number Theory. Springer-Verlag.
• 12: Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
• 13: Shapiro, H. N. 1983. Introduction to the Theory of Numbers. Pure and Applied Mathematics. John Wiley & Sons Inc.
• 14: Markus Wenzel, Type Classes and Overloading in Higher-Order Logic, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, p.307-322, August 19-22, 1997
• 15: Wenzel, M. 2002. Isabelle/isar---a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut für Informatik, Technische Universität München.
• 16: Freek Wiedijk, The Seventeen Provers of the World: Foreword by Dana S. Scott (Lecture Notes in Computer Science / Lecture Notes in Artificial Intelligence), Springer-Verlag New York, Inc., Secaucus, NJ, 2006

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Experimentation, Theory, Verification

Keywords:
Prime number theorem, formal verification