We prove that if conditions I-II (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$ do not have p-size proofs in Extended Frege system EF, then $P \ne NP$.

I. $S^1_2$ proves that there is a function $g\in E$ hard to approximate by subexponential-size circuits.

II. (Learning from the non-existence 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 \ne 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... more