|Abstract||On September 6, 2004, using the Isabelle proof assistant, I veriﬁed the following statement: (%x. pi x * ln (real x) / (real x)) ----> 1 The system thereby conﬁrmed that the prime number theorem is a consequence of the axioms of higher-order logic together with an axiom asserting the existence of an inﬁnite set. All told, our number theory session, including the proof of the prime number theorem and supporting libraries, constitutes 673 pages of proof scripts, or roughly 30,000 lines. This count includes about 65 pages of elementary number theory that we had at the outset, developed by Larry Paulson and others; also about 50 pages devoted to a proof of the law of quadratic reciprocity and properties of Euler’s ϕ function, neither of which are used in the proof of the prime number theorem. The page count does not include the basic HOL library, or properties of the real numbers that we obtained from the HOL-Complex library.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
Chris Freiling (1986). Axioms of Symmetry: Throwing Darts at the Real Number Line. Journal of Symbolic Logic 51 (1):190-200.
Takahito Aoto (1999). Uniqueness of Normal Proofs in Implicational Intuitionistic Logic. Journal of Logic, Language and Information 8 (2):217-242.
Alexander S. Karpenko (1989). Characterization of Prime Numbers in Łukasiewicz's Logical Matrix. Studia Logica 48 (4):465 - 478.
Added to index2009-03-12
Total downloads23 ( #60,181 of 722,864 )
Recent downloads (6 months)1 ( #60,917 of 722,864 )
How can I increase my downloads?