A formally verified proof of the prime number theorem

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.
23 pages

Keywords

Artificial Intelligence, Logic in Computer Science, Symbolic Computation, F.4.1; I.2.3

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/101859

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0509025
 http://arxiv.org/abs/cs/0509025

Collections

arXiv