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)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Axioms of Symmetry: Throwing Darts at the Real Number Line.Chris Freiling - 1986 - Journal of Symbolic Logic 51 (1):190-200.
Uniqueness of Normal Proofs in Implicational Intuitionistic Logic.Takahito Aoto - 1999 - Journal of Logic, Language and Information 8 (2):217-242.
Characterization of Prime Numbers in Łukasiewicz's Logical Matrix.Alexander S. Karpenko - 1989 - Studia Logica 48 (4):465 - 478.
Added to index2009-03-12
Total downloads45 ( #115,450 of 2,168,154 )
Recent downloads (6 months)1 ( #346,757 of 2,168,154 )
How can I increase my downloads?