Asperti, Andrea; Ricciotti, Wilmer A proof of Bertrand’s postulate. (English) Zbl 1451.68331 J. Formaliz. Reason. 5, No. 1, 37-57 (2012). Summary: 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. Cited in 2 Documents MSC: 68V20 Formalization of mathematics in connection with theorem provers 11A41 Primes 11N05 Distribution of primes 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) Software:Matita PDFBibTeX XMLCite \textit{A. Asperti} and \textit{W. Ricciotti}, J. Formaliz. Reason. 5, No. 1, 37--57 (2012; Zbl 1451.68331) Full Text: DOI