We study the problem of proving in weak theories of Bounded Arithmetic the theorem that there are arbitrarily large prime
numbers. We show that the theorem can be proved by some “minimal” reasoning (i.e., in the theory IΔ
0
) using concepts such as (the logarithm) of a binomial coefficient. In fact we prove Bertrand’s Postulate (that there is at
least a prime number between n and 2n, for all n > 1) and the fact that the number of prime numbers between n and 2n is of order Θ(n/ln (n)). The proofs that we formalize are much simpler than several existing formalizations, and our theory turns out to be a sub-theory
of a recent theory proposed by Woods and Cornaros that extends IΔ
0
by a special counting function.