### Abstract

We prove that if conditions (a)-(b) (below) hold and there is a sequence of Boolean functions f_n hard to approximate by p-size circuits such that p-size circuit lower bounds for f_n douel not have p-size proofs in Extended Frege system EF, then P≠NP.

(a) (Explicit circuit lower bound) $S^1_2$ proves that a concrete function in E is hard to approximate by subexponential-size circuits.

(b) (Learning from the nonexistence of OWFs) $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits learning p-size circuits over the uniform distribution, with membership queries.

Here, $S^1_2$ is Buss’s theory of bounded arithmetic formalizing p-time reasoning.

Further, we show that any of the following assumptions implies that P≠NP, if EF is not p-bounded:

1. (Feasible anticheckers) $S^1_2$ proves that a p-time function generates anticheckers for SAT.

2. (Witnessing NP$\not\subseteq$P/poly) $S^1_2$ proves that a p-time function witnesses an error of each p-size circuit which fails to solve SAT.

3. (OWF from NP$\not\subseteq$P/poly & hardness of E) Condition (a) holds and $S^1_2$ proves that a p-time reduction transforms circuits breaking one-way functions to p-size circuits computing SAT.

The results generalize to stronger theories and proof systems.

This is joint work with Rahul Santhanam.