[Proof Complexity] Prague seminar on Monday - Jan Pich

[thapen]

Jan Pich will speak at our logic seminar next Monday, December 12, at 
16:00 Prague time.

It will be broadcast on zoom. To join use the link
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

-------------------------------------------------------------------------

Title: Towards P != NP from Extended Frege lower bounds

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 
function witnesses an error of each p-size circuit which fails to solve 
SAT.
3. (OWFs from $NP\not\subseteq P/poly$ & hardness of 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.

This is joint work with Rahul Santhanam.


For more information see the seminar web page at
https://calendar.math.cas.cz/logic-seminar-actual .