Towards P≠NP from Extended Frege Lower Bounds
10Ján Pich (University of Oxford)
https://simons.berkeley.edu/talks/jan-pich-university-oxford-2023-03-21-0
Proof Complexity and Meta-Mathematics
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.