A formally verified proof of the prime number theorem

2005/09/09 by Jeremy Avigad, Kevin Donnelly, Avigad, Jeremy +6 · 1 citation
Computer Science · Mathematics · #Analytic Number Theory Research #Artificial Intelligence (cs.AI) #F.4.1 #FOS: Computer and information sciences #History and Theory of Mathematics #I.2.3 #Logic in Computer Science (cs.LO) #Mathematics and Applications #Symbolic Computation (cs.SC) #cs.AI #cs.LO #cs.SC

paper · pdf · doi:10.48550/arxiv.cs/0509025

23 pages

openalex publication_date 2005/09/09 · arxiv created 2006/04/06 · arxiv updated 2009/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'ee 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"os in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

Cited by

• Universal Gluing and Contextual Choice: Categorical Logic and the Foundations of Analytic Approximation

Related

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