article

A formally verified proof of the prime number theorem

Authors:

Kevin Donnelly,

Paul RaffAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 9, Issue 1

Pages 2 - es

https://doi.org/10.1145/1297658.1297660

Published: 01 December 2007 Publication History

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.

Digital Library

[11]

Nathanson, M. B. 2000. Elementary Methods in Number Theory. Springer-Verlag.

[12]

Nipkow, T., Paulson, L. C., and Wenzel, M. 2002. Isabelle/HOL. A proof assistant for higher-order logic. Lecture Notes in Computer Science, vol. 2283. Springer-Verlag.

Digital Library

[13]

Shapiro, H. N. 1983. Introduction to the Theory of Numbers. Pure and Applied Mathematics. John Wiley & Sons Inc.

[14]

Wenzel, M. 1997. Type classes and overloading in higher-order logic. In Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), E. Gunter and A. Felty, Eds. NJ, 307--322.

Digital Library

[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]

Wiedijk, F. 2006. The Seventeen Provers of the World. Springer-Verlag.

Digital Library

Cited By

Song SYao B(2025)Formalization of the Prime Number Theorem with a Remainder TermJournal of Automated Reasoning10.1007/s10817-025-09718-969:1Online publication date: 4-Feb-2025
https://doi.org/10.1007/s10817-025-09718-9
Mietchen DJeschke JHeger T(2024)Introducing Hypothesis DescriptionsResearch Ideas and Outcomes10.3897/rio.10.e11980510Online publication date: 1-Feb-2024
https://doi.org/10.3897/rio.10.e119805
Platzer A(2024)Intersymbolic AILeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_11(162-180)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_11
Show More Cited By

Index Terms

A formally verified proof of the prime number theorem
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Models of computation
    1. Computability

Recommendations

Proof-checking metamathematics (theorem-proving)
Revisiting Gauss's analogue of the prime number theorem for polynomials over a finite field

In 1901, von Koch showed that the Riemann Hypothesis is equivalent to the assertion that@__ __p=
Counting polynomial roots in Isabelle/HOL: a formal proof of the Budan-Fourier theorem
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs

Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 9, Issue 1

December 2007

250 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/1297658

Issue’s Table of Contents

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 December 2007

Published in TOCL Volume 9, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

52
Total Citations
View Citations
784
Total Downloads

Downloads (Last 12 months)17
Downloads (Last 6 weeks)2

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Song SYao B(2025)Formalization of the Prime Number Theorem with a Remainder TermJournal of Automated Reasoning10.1007/s10817-025-09718-969:1Online publication date: 4-Feb-2025
https://doi.org/10.1007/s10817-025-09718-9
Mietchen DJeschke JHeger T(2024)Introducing Hypothesis DescriptionsResearch Ideas and Outcomes10.3897/rio.10.e11980510Online publication date: 1-Feb-2024
https://doi.org/10.3897/rio.10.e119805
Platzer A(2024)Intersymbolic AILeveraging Applications of Formal Methods, Verification and Validation. Software Engineering Methodologies10.1007/978-3-031-75387-9_11(162-180)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-75387-9_11
Avigad J(2024)Automated Reasoning for MathematicsAutomated Reasoning10.1007/978-3-031-63498-7_1(3-20)Online publication date: 3-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-63498-7_1
Söldner RPlump D(2023)Mechanised DPO Theory: Uniqueness of Derivations and Church-Rosser TheoremGraph Transformation10.1007/978-3-031-36709-0_7(123-142)Online publication date: 19-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-36709-0_7
Nipkow TEberl MHaslbeck M(2020)Verified Textbook AlgorithmsAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_2(25-53)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_2
Chatzikyriakidis SLuo Z(2020)ReferencesFormal Semantics in Modern Type Theories10.1002/9781119489252.refs(209-223)Online publication date: 11-Dec-2020
https://doi.org/10.1002/9781119489252.refs
Lewis RMahboubi AMyreen M(2019)A formal proof of Hensel's lemma over the p-adic integersProceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3293880.3294089(15-26)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3293880.3294089
Chan HNorrish M(2019)Proof PearlJournal of Automated Reasoning10.1007/s10817-017-9438-062:2(171-192)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10817-017-9438-0
Carl M(2019)Formal and Natural Proof: A Phenomenological ApproachReflections on the Foundations of Mathematics10.1007/978-3-030-15655-8_14(315-343)Online publication date: 12-Nov-2019
https://doi.org/10.1007/978-3-030-15655-8_14
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents