Bertrand's Postulate

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

17 January 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

Depends On

Used by