Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems

Published on ● Video Link: https://www.youtube.com/watch?v=QrJMLFHCSTk



Duration: 1:03:41
265 views
4


Iddo Tzameret (Imperial College London)
https://simons.berkeley.edu/talks/iddo-tzameret-imperial-college-london-2023-03-22-0
Proof Complexity and Meta-Mathematics

I will describe the state-of-the-art in proof complexity lower bounds achieved via reductions to algebraic circuit lower bounds. We shall see that in the world of algebraic proof systems, when not insisting that hard instances are in CNF, major problems that are open in the corresponding world of boolean (Frege-style) systems, are already solved. I'll present some open problems and directions for further study, including barriers to obtaining CNF hard instances (which would solve major open problems in proof complexity).




Other Videos By Simons Institute for the Theory of Computing


2023-03-24Weak Versions of Extended Resolution
2023-03-24CDCL vs Resolution: The Picture in QBF
2023-03-24Read-Once Branching Programs as Proof Lines
2023-03-24Connections Between QBF Proof Complexity and Circuit Complexity
2023-03-24Certifying Combinatorial Solving Using Cutting Planes with Strengthening Rules
2023-03-24On the Dominance-Based Strengthening Rule
2023-03-23On the Problems Related to Waring Rank and Border Waring Rank
2023-03-23Lower Bounds Against Non-Commutative Models of Algebraic Computation
2023-03-23Natural Proofs in Algebraic Circuit Complexity
2023-03-23Variety Membership Testing, Algebraic Natural Proofs, and Geometric Complexity Theory
2023-03-22Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems
2023-03-22Indistinguishability Obfuscation via Mathematical Proofs of Equivalence
2023-03-22Towards P≠NP from Extended Frege Lower Bounds
2023-03-22Indistinguishability Obfuscation, Range Avoidance, and Bounded Arithmetic
2023-03-22Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
2023-03-21Consistency of NEXP Not in P/poly in a Strong Theory
2023-03-21Lifting to Parity Decision Trees via Stifling (with applications to proof complexity)
2023-03-21A Lower Bound for k-DNF Resolution on Random CNF Formulas via Expansion
2023-03-21The Hitting Proof System
2023-03-21Random log(n)-CNF are Hard for Cutting Planes (Again)
2023-03-20Lower Bounds Against PC With Extension Variables



Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Proof Complexity and Meta-Mathematics
Iddo Tzameret