|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)|
|Categories||No categories specified (fix it)|
|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).
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 ( #145,761 of 549,753 )
Recent downloads (6 months)2 ( #37,450 of 549,753 )
How can I increase my downloads?