Bertrand's postulate

Julian Biendarra and Manuel Eberl 🌐 with contributions from Lawrence C. Paulson 🌐

January 17, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Bertrand's postulate is an early result on the distribution of prime numbers: For every positive integer n, there exists a prime number that lies strictly between n and 2n. The proof is ported from John Harrison's formalisation in HOL Light. It proceeds by first showing that the property is true for all n greater than or equal to 600 and then showing that it also holds for all n below 600 by case distinction.


BSD License


Session Bertrands_Postulate