Proof complexity is a vibrant area in the intersection of computational complexity, algorithms and mathematical logic exploring the inherent difficulty of proving mathematical theorems. This workshop aims to cover both traditional topics and emerging trends in the field such as lower bounds on lengths of proofs, bounded arithmetic, model theory & forcing, SAT & QBF solving, connections to TFNP and algebraic complexity, lifting theorems and meta-mathematics of complexity theory.
The workshop will take place on 11-13 August at the University of Oxford. The program will consist of talks by selected speakers and will include ample time for discussions.
Previous edition of the workshop: Proof Complexity 2024.
To register for the workshop, please use the following Registration Form.
Registration is now closed. If you wish to participate and have not yet registered, please contact the organizers.
Program
Talks are either 25 or 40 minutes in total. Speakers are asked to leave at least 3 minutes at the end of their talk for questions.| 9:30-10:00 Monday Morning Coffee | |
| Monday: Session 1 — 10:00-11:30 | |
| 40 min | Algebraic proof complexity: state of the art Iddo Tzameret |
|---|---|
| 25 min | Improved lifting theorem Shuo Pang |
| 25 min | The proof analysis problem Noel Arteche |
| Monday: Session 2 — 14:00-15:30 | |
| 40 min | Monotone circuit complexity of perfect matching Bruno Cavalar |
| 25 min | Formalizing the AKS primality algorithm in bounded arithmetic Raheleh Jalali |
| 25 min | Pseudodeterministic communication complexity Anastasia Sofronova |
| 15:30-16:00 Monday Afternoon Coffee Break | |
| Monday: Session 3 — 16:00-17:30 | |
| 40 min | Provability of Circuit Size Hierarchy in Constant Lines of $\mathsf{VPV}$ Marco Carmosino |
| 25 min | A Logspace Constructive Proof of $\mathsf{L} = \mathsf{SL}$ Antonina Kolokolova |
| 25 min | Lower Bounds against the Ideal Proof System in Finite Fields Tal Elbaz |
| 9:30-10:00 Tuesday Morning Coffee | |
| Tuesday: Session 1 — 10:00-11:30 | |
| 40 min | Local Enumeration, SSETH, and Depth-3 Lower Bounds Navid Talebanfard |
| 25 min | Bounded-Assembler: Programming in Bounded Arithmetic Stefan Grosser |
| 25 min | Symmetric Proofs in the Ideal Proof System Benedikt Pago |
| Tuesday: Session 2 — 14:00-15:30 | |
| 40 min | Recent advances in Resolution over parities Dmitry Itsykson |
| 25 min | Uniform Counting Principle v.s. injective PHP in the relativized bounded arithmetic $T_{2}(R)$ Eitetsu Ken |
| 25 min | Resolution Proof Complexity for Embedding a Length-$(n + 1)$ Path into Expanders. Aleksandr Shekhovtsov |
| 15:30-16:00 Tuesday Afternoon Coffee Break | |
| Tuesday: Session 3 — 16:00-17:30 | |
| 25 min | Weak Rank Principle I Svyatoslav Gryaznov |
| 25 min | Weak Rank Principle II Hanlin Ren |
| 40 min | Open Problems Session Chair: Nicola Galesi |
| 9:30-10:00 Wednesday Morning Coffee | |
| Wednesday: Session 1 — 10:00-11:30 | |
| 40 min | On the consistency of stronger lower bounds for NEXP Neil Thapen |
| 25 min | $\mathsf{AC}[p]$-Frege Cannot Efficiently Prove that Constant-Depth Algebraic Circuit Lower Bounds are Hard Jiaqi Lu |
| 25 min | Lower bounds for CSP hierarchies through ideal reduction Jonas Conneryd |
| Wednesday: Session 2 — 14:00-15:30 | |
| 40 min | Searching for falsified clauses in random $(\log n)$-CNFs is hard for randomized communication Dmitry Sokolov |
| 25 min | Jump Operators Erfan Khaniki |
| 25 min | Towards an Alternative Foundation for Feasible Mathematics Amir Tabatabai |
| 15:30-16:00 Wednesday Afternoon Coffee Break | |
| Wednesday: Session 3 — 16:00-17:40 | |
| 25 min | Wide Limits: An Alternative View of Forcing in Bounded Arithmetic Ondrej Jezil |
| 25 min | Provably total functions in the polynomial hierarchy Christophe Marciot |
| 25 min | Stifling the non-locality of parities Suhail Sherif |
| 25 min | Towards complex analysis in $\mathsf{VTC}^0$ Emil Jeřábek |
Venue
Lecture Theatre B (LTB) & Atrium, Wolfson building, Department of Computer Science, University of Oxford.
Address: Wolfson building, Parks road, Oxford, OX1 3QD, UK
How to get here
Accommodation
Oxford colleges provide accommodation for visitors in August, see e.g. Keble College (nearest to the department), Wolfson College or St Anne's College. To book a room please use conference-oxford or the website of the college of your choice. Hotels and AirBnB can offer a great alternative.
Speakers
- Noel Arteche
- Bruno Cavalar
- Marco Carmosino
- Jonas Conneryd
- Tal Elbaz
- Noah Fleming
- Stefan Grosser
- Svyatoslav Gryaznov
- Dmitry Itsykson
- Raheleh Jalali
- Emil Jeřábek
- Ondrej Jezil
- Eitetsu Ken
- Erfan Khaniki
- Antonina Kolokolova
- Jiaqi Lu
- Christohe Marciot
- Benedikt Pago
- Shuo Pang
- Hanlin Ren
- Aleksandr Shekhovtsov
- Suhail Sherif
- Anastasia Sofronova
- Dmitry Sokolov
- Amir Tabatabai
- Navid Talebanfard
- Neil Thapen
- Iddo Tzameret
- Marco L. Carmosino, IBM
- Ján Pich, University of Oxford
- Iddo Tzameret, Imperial College London