Bertrand's postulate

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

January 17, 2017


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