I have a simple question. Can a bounded arithmetic, say $S^1_2$ prove prime factorization? I think this is an open problem, because if $S^1_2$ can prove prime factorization then prime factorization is $P$, which is open. But I have a vague recollection that some paper or textbook says prime factorization can be proven by a bounded arithmetic, yet it does not entail prime factorization is $P$.
Is this just my incorrect memory or do you know a reference?
A similar theorem is Cook and Nguyen, exercise VI.4.4, which is to prove in the system $V_1$ that every binary-encoded integer $X \geq 2$ can be written as a product of primes. This result is from Jerabek's thesis, where he gives a detailed proof in what I take also to be $V_1$.
Part of the exercise is to explain why this doesn't yield a $P$ solution, but to be truthful I am drawing a blank today.