First, let me discuss the precise open question and why it is interesting to logicians. Then I will discuss potential ramifications outside of pure logic.

The main open question is whether the theory IΔ_{0} can prove the existence of arbitrarily large primes. The theory IΔ_{0} is the theory over the language of basic arithmetic ($0,1,+,\times,{\leq}$, together with their usual defining axioms) where induction is limited to bounded formulas (Δ_{0} formulas): formulas wherein all quantifiers are of the bounded form $\forall x(x \leq t \rightarrow \cdots)$ and $\exists x(x \leq t \land \cdots)$ where $t$ is a term of the language possibly involving variables other than $x$. While this theory has been around for quite some time, one of the earliest papers studying this system in detail is Paris & Wilkie *On the scheme of induction for bounded arithmetic formulas* [Ann. Pure Appl. Logic 35 (1987), no. 3, 261–302, MR904326]. The currently open question regarding the unboundedness of primes occurs there, probably for the first time in print.

Why is this question interesting to logicians? There is a standard fact about the proof theory of ∀∃-formulas which explains the interest. Over IΔ_{0}, this fact takes the following form due to Parikh:

**Fact.** If IΔ_{0} proves $\forall x \exists y \phi(x,y)$, where $\phi(x,y)$ is a bounded formula, then IΔ_{0} proves $\forall x \exists y(y \leq t(x) \land \phi(x,y))$ where $t(x)$ is a term of the language (i.e. a polynomial in $x$).

Thus, IΔ_{0} cannot prove certain statements such as $\forall x \exists y (2^x = y)$ since $2^x$ grows faster than any polynomial. (Here, $2^x = y$ is an abbreviation for a bounded formula that expresses the properties of the exponential function $2^x$. That formula is rather complex, so I will not explain it here.) In fact, any proof that involves functions of exponential growth at intermediate stages cannot be formalized in IΔ_{0} because of this. This applies in particular to Euclid's proof which takes a rather large product of primes relative to the input $x$ in order to prove that there is a prime larger than $x$. However, by Bertrand's Postulate, the formula $\forall x \exists y(\mathrm{prime}(y) \land y \geq x)$ does not by itself impose exponential growth. Thus, the fact leaves open the question whether some other proof of the infinitude of primes can be formalized in IΔ_{0}.

What are potential ramifications outside of logic? A natural question to ask about primes is whether there is some kind of efficient formula for producing large primes. (Cf. the Polymath 4 Project.) One can ask further about the growth rate and the computational complexity of such a function. Proof mining techniques show that if IΔ_{0} proves the infinitude of primes, then there must be a relatively simple function of moderate growth rate to produce large primes. In fact, there must be such a function that produces primes provably in IΔ_{0}.

The existence of such a function should not be a surprise. Indeed, the simple function $p(x)$ that returns the first prime greater than $x$ has very moderate growth rate by Bertrand's Postulate. However, the function produced by a proof of the unboundedness of primes in IΔ_{0} will have other important characteristics. In particular, it will have rather low computational complexity. The precise relationship between IΔ_{0} and computational complexity is a little subtle and I don't want to make this statement more precise here. (Some details were added below.) However, there are good reasons to believe that such a proof could yield a polynomial time computable function of moderate growth that produces large primes, which would be a major breakthrough.

What can we say if there is no IΔ_{0} proof of the existence of arbitrarily large primes? Well, for one thing, a model of IΔ_{0} where primes are bounded would be a rather interesting object with potential applications to the structure theory of integral domains. However, it turns out that there is not much one can say here about the standard model, but the reason is subtle.

The key problem is the definition of prime number. In the discussion above, I implicitly assumed the standard definition $\mathrm{prime}(x)$ iff $$x > 1 \land (\forall y, z \leq x)(x = yz \rightarrow y = 1 \lor z = 1).$$ However, there are other potential definition of primes. For example, one could define prime numbers as those which pass the AKS primality test. These various equivalent definitions are not necessarily equivalent over IΔ_{0}. Therefore, it is possible that IΔ_{0} fails to prove the existence of arbitrarily large "traditional primes" but that IΔ_{0} does prove the existence of arbitrarily large "AKS primes." Since the standard model can't tell the difference between these two notions of primality, this could still give an efficient way to produce large primes as discussed above.

Let me clarify the relationship between proofs in IΔ_{0} and computational complexity. The polynomial hierarchy is closely tied to slightly different systems of bounded arithmetic, namely the systems $S^n_2$, $T^n_2$ pioneered by Sam Buss. Note that these are somewhat orthogonal to IΔ_{0}. On the one hand, these systems include the smash function $x \# y = 2^{|x||y|}$ which is not provably total in IΔ_{0}. On the other hand, the amount of induction in these systems is even more restricted than in IΔ_{0}.

It is hard to give a precise relationship between time complexity and proofs in IΔ_{0}. The claims I made above are rather based on the (admittedly optimistic) expected success of proof mining on a hypothetical proof the unboundedness of primes in IΔ_{0}.

In any case, there is an inherent weakness to this approach. Complexity theorists do not impose limits on the amount of induction they use in their proofs. For example, complexity theorists will freely use the equivalence of "traditional primes" and "AKS primes" in their arguments. Therefore, the existence of a simple way to generate large primes is not at all equivalent to the existence of a proof of the existence of arbitrarily large primes in IΔ_{0} or other systems of bounded arithmetic.