Email Gateway (Aug 22 2022 at 14:58): Email Gateway (Aug 22 2022 at 14:58):From: Lawrence Paulson <lp15@cam.ac.uk>
We have a new and quite unusual contribution by Julian Biendarra and Manuel Eberl:
"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.”
It’s an important result and the proof involves reflection along with a specific list of prime numbers. You will find the entry here:
https://www.isa-afp.org/entries/Bertrands_Postulate.shtml
Larry Paulson
Last updated: Apr 25 2024 at 08:20 UTC