  We prove the first unconditional consistency result for superpolynomial
circuit lower bounds with a relatively strong theory of bounded arithmetic.
Namely, we show that the theory V$^0_2$ is consistent with the conjecture that
NEXP $\not\subseteq$ P/poly, i.e., some problem that is solvable in
non-deterministic exponential time does not have polynomial size circuits. We
suggest this is the best currently available evidence for the truth of the
conjecture. The same techniques establish the same results with NEXP replaced
by the class of problems that are decidable in non-deterministic barely
superpolynomial time such as NTIME$(n^{O(\log\log\log n)})$. Additionally, we
establish a magnification result on the hardness of proving circuit lower
bounds.
