What's the history of the result that $p_{n+1} < p_n^2$, and how difficult is the proof?

Question

In Edsger Dijkstra's monograph "Notes on Structured Programming", he describes a simple imperative program for generating an array of the first $n$ primes. For each prime $p_n$, it finds the next prime by checking each odd $j \gt p_n$, to see if it has a prime divisor $d$ in the range $2 \lt d \le \sqrt j$. The algorithm draws these candidates from the array of prime numbers it has been constructing, which at any given iteration contains the primes between $2$ and $p_n$ inclusive, so there is an implicit assumption is that $\sqrt j \le p_n$ (the algorithm iterates over the array of primes up to $p_n$ with the only termination conditions being $d|j$ or $d > \sqrt j$, so if $\sqrt j$ could be $\ge p_n$ we risk reading past the end of the array). Quoting Dijkstra:

In all humility I quote Don Knuth's comment on an earlier version of this program, where I took this fact for granted:

"Here you are guilty of a serious omission! Your program makes use of a deep result of number theory, namely that if $p_n$ denotes the $n$th prime number we always have $p_{n+1} < p_n^2$."

So I'm curious about the history of this "deep result", and how difficult the proof is.

Answer 1

I am uncertain of that particular proof, but I know a few proofs of Bertrand's Postulate. Bertrand's says that for all $n > 3$, there is a prime between $n$ and $2n$. In particular, this means that given a prime $p_0$, there is another prime $p_1$ s.t. $p_0 < p_1 < 2p_0$ As $2 < p_0$, we then have that there is a $p_1$ s.t.

$$p_0 < p_1 < 2p_0 < p_0 ^2$$

I think the Wikipedia proof is not so bad. Bertrand actually proved his conjecture himself in the late 1800's, and there are many proofs. Ramanujan made one, Erdos improved up it. There are also many better results and asymptotic results - I have used Pierre Dusart's improvement before, which says that for sufficiently large x (larger than 3275), there is a prime between $x$ and $x + \dfrac{x}{1 + 2\log^2 x}$. That's very intense!

But that idea is somewhat deep, and it relates to the Prime Number Theorem on the distribution of primes (which I would call very deep).

Answer 2

Actually, the program as described requires no such assumption. Remember, it starts from the last prime found so far and checks every (odd) number in turn to see if it is composite; therefore, the first non-composite number thus found must be the next prime.

The primality check merely makes use of the following rather trivial result:

Lemma: Every composite number is divisible by some prime no greater than its square root.

Proof: We need to show that every composite number must have a (possibly non-prime) divisor no greater than its square root; this divisor must then have a prime factor no greater than itself. To prove this, assume the contrary, i.e. that there exists a composite number $n$ such that its smallest proper divisor $k$ satisfies $k > \sqrt n$. But then $n/k < \sqrt n$ is also a divisor of $n$, which is a contradiction.

---

Edit: Sorry, I see my mistake now. It is indeed not trivial to show that the program will never read past the end of the list of primes if that's not checked for. I'll leave my answer up for a record of the conversation, but I'll mark it as community wiki. Please don't upvote it.