|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 Erdos in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.|
|Keywords||No keywords specified (fix it)|
No categories specified
(categorize this paper)
|Through your library||Only published papers are available at libraries|
Similar books and articles
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Jeremy Avigad (2006). Mathematical Method and Proof. Synthese 153 (1):105 - 159.
J. Todd Wilson (2001). An Intuitionistic Version of Zermelo's Proof That Every Choice Set Can Be Well-Ordered. Journal of Symbolic Logic 66 (3):1121-1126.
Alexander S. Karpenko (1989). Characterization of Prime Numbers in Łukasiewicz's Logical Matrix. Studia Logica 48 (4):465 - 478.
Konstantine Arkoudas & Selmer Bringsjord (2007). Computers, Justification, and Mathematical Knowledge. Minds and Machines 17 (2):185-202.
Carlo Cellucci (2008). Why Proof? What is a Proof? In Giovanna Corsi & Rossella Lupacchini (eds.), Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, pp. 1-27. Springer.
Colin Mclarty (2010). What Does It Take to Prove Fermat's Last Theorem? Grothendieck and the Logic of Number Theory. Bulletin of Symbolic Logic 16 (3):359-377.
Added to index2010-09-14
Total downloads6 ( #154,770 of 722,935 )
Recent downloads (6 months)2 ( #36,864 of 722,935 )
How can I increase my downloads?