Carnegie Mellon University
Browse
file.pdf (265.08 kB)

A Formally Verified Proof of the Prime Number Theorem

Download (265.08 kB)
journal contribution
posted on 2007-01-01, 00:00 authored by Jeremy AvigadJeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
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 Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

History

Publisher Statement

This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution.

Date

2007-01-01

Usage metrics

    Categories

    Keywords

    Prime number theoremformal verification

    Licence

    In Copyright

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC