We prove that the conjecture NEXP \not\subseteq P/poly is true in a model of the relatively strong theory of bounded arithmetic V02. Concretely, there is a model of V02 in which the canonical NEXP-complete problem cannot be solved by polynomial-size circuits. To our knowledge, this is the first unconditional consistency result for superpolynomial circuit lower bounds in a strong theory of bounded arithmetic -- previous consistencies were conditioned on unproved conjectures, or for fixed-polynomial lower bounds. The theory V02 includes Buss' hierarchy T2, where the theory S12 for polynomial-time reasoning sits at its first level, and includes Jerabek's theoris APC1 and APC2 for a approximate counting reasoning. In particular, it is known that a significant part of contemporary complexity theory can be formalized in V02. We view this as supporting the claim that the consistency of the conjecture NEXP \not\subseteq P/poly in V02 is the strongest available evidence that it is actually true.

Based on joint work with Sam Buss (UCSD) and Moritz Mueller (U.Passau).