A formally verified proof of the prime number theorem

2007/12/01 by Jeremy Avigad, K. Donnelly, David Gray +1 · 5 citations
Mathematics · #History and Theory of Mathematics #Mathematics and Applications #Analytic Number Theory Research

paper · doi:10.1145/1297658.1297660

openalex publication_date 2007/12/01 · openalex created_date 2019/06/27 · openalex updated_date 2026/07/28

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.

Cited by

• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
• Formalizing an Analytic Proof of the Prime Number Theorem
• Proof assistants: History, ideas and future
• Combining decision procedures for the reals
• First-order logic [wikipedia]
• Prime number theorem [wikipedia]

Related

• A formally verified proof of the prime number theorem
• Formalization of the prime number theorem and Dirichlet's theorem
• Note on the Prime Number Theorem
• An alternative proof of the Dirichlet prime number theorem
• A Conjecture about the Density of Prime Numbers