Academic Journals Database
Disseminating quality controlled scientific knowledge

A proof of Bertrand's postulate

Author(s): Andrea Asperti | Wilmer Ricciotti

Journal: Journal of Formalized Reasoning
ISSN 1972-5787

Volume: 5;
Issue: 1;
Start page: 37;
Date: 2012;
Original page

Keywords: Bertrand's postulate | Chebyshev's functions | distribution of prime numbers | Matita | interactive theorem proving

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.
RPA Switzerland

RPA Switzerland

Robotic process automation


Tango Rapperswil
Tango Rapperswil