Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems
summary
Survey of state-of-the-art reductions showing that lower bounds for algebraic circuits yield proof complexity lower bounds via the Ideal Proof System (IPS); main technical move converts a refutation into a single polynomial certificate and reduces C‑IPS lower bounds to functional circuit lower bounds for g(x)=1/f(x) over the Boolean cube. Unconditional separations appear for restricted classes (e.g. read-once ABPs, multilinear formulas, constant‑depth circuits) using coefficient‑matrix rank (Nisan ’91 style) and evaluation‑dimension tricks; major obstacle remains producing CNF hard instances and handling coefficient bit‑size.
AI-written summary · about
chapters (10)
- 0:00Introduction and overview
- 2:29Proof complexity basics
- 10:22Expanding to algebraic systems
- 15:42Ideal proof systems (IPS)
- 22:24Defining IPS refutations
- 27:45Solving open problems via IPS
- 37:13Hard instances in algebra
- 41:27Lower bound templates
- 51:28Advanced lower bound techniques
- 1:00:48Discussion and conclusion
related talks
37mJourney with Eric Allender: From Turing Machines to Circuits, and Back
55mLower Bounds for Subgraph Isomorphism and Consequences in First-Order Logic
53mNew Lower Bounds and Derandomization for ACC, and a...
01h 17mInapproximability of Constraint Satisfaction Problems V
18mOn the Verification of a Subgraph Construction Algorithm
54mConstraints, Gadgets, and Invariants
01h 01mThe Gospel According to TCS
01h 17mInapproximability of Constraint Satisfaction Problems III