文章基本信息

标题：A proof of Bertrand's postulate
本地全文：下载
作者：Andrea Asperti ; Wilmer Ricciotti
期刊名称：Journal of Formalized Reasoning
印刷版ISSN：1972-5787
出版年度：2012
卷号：5
期号：1
页码：37-57
DOI：10.6092/issn.1972-5787/3406
语种：English
出版社：Alma Mater Studiorum - University of Bologna
摘要：We discuss the formalization, in the Matita Interactive Theorem Prover, of some results by Chebyshev concerning the distribution of prime numbers, subsuming, as a corollary, Bertrand's postulate. Even if Chebyshev's result has been later superseded by the stronger prime number theorem, his machinery, and in particular the two functions psi and theta still play a central role in the modern development of number theory. The proof makes use of most part of the machinery of elementary arithmetics, and in particular of properties of prime numbers, gcd, products and summations, providing a natural benchmark for assessing the actual development of the arithmetical knowledge base.