  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 a concrete function in ${\sf E}$ is hard to
approximate by subexponential-size circuits.
  II. [Learning from $\neg\exists$ OWF.] $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
function witnesses an error of each p-size circuit which fails to solve SAT.
  3. [OWF from $NP\not\subseteq P/poly$ $\&$ hardness of ${\sf E}$.] Condition
I 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.
