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.
Program (Tentative)
| Monday: Session 1 | |
| 40 min |
Algebraic proof complexity: state of the art.
Iddo Tzameret |
|---|---|
| 25 min |
Bounded-Assembler: Programming in Bounded Arithmetic Stefan Grosser |
| 25 min |
The proof analysis problem Noel Arteche |
| Monday: Session 2 | |
| 40 min | Noah Fleming and Marco Carmosino |
| 25 min |
Pseudodeterministic communication complexity Anastasia Sofronova |
| 25 min |
Resolution Proof Complexity for Embedding a Length-$(n + 1)$ Path into Expanders. Aleksandr Shekhovtsov |
| Monday: Session 3 | |
| 40 min |
Unconditional Line-Count Separations in Bounded Arithmetic Marco Carmosino |
| 25 min |
Improved lifting theorem Shuo Pang |
| 25 min |
Lower Bounds against the Ideal Proof System in Finite Fields Tal Elbaz |
| Tuesday: Session 1 | |
| 40 min | TBD |
| 25 min |
Formalizing the AKS primality algorithm in bounded arithmetic Raheleh Jalali |
| 25 min | Benedikt Pago |
| Tuesday: Session 2 | |
| 40 min |
Recent advances in Resolution over parities Dmitry Itsykson |
| 25 min |
Generalized Linial-Nisan conjecture is false for DNFs Artur Riazanov |
| 25 min | Monotone circuit complexity of perfect matching Bruno Cavalar |
| Tuesday: Session 3 | |
| 40 min | TBD |
| 25 min |
The Weak Rank Principle: Lower Bounds and Applications Svyatoslav Gryaznov |
| 25 min | Hanlin Ren |
| Wednesday: Session 1 | |
| 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 | |
| 40 min |
Searching for falsified clauses in random $(\log n)$-CNFs is hard for randomized communication Dmitry Sokolov |
| 25 min | Erfan Khaniki |
| 25 min |
Towards an Alternative Foundation for Feasible Mathematics Amir Tabatabai |
| Wednesday: Session 3 | |
| 40 min | TBD |
| 25 min |
Stifling the non-locality of parities Suhail Sherif |
| 25 min |
Provably total functions in the polynomial hierarchy Christohe Marciot |
| 25 min |
Towards complex analysis in $\mathsf{VTC}^0$ Emil Jeřábek |
Speakers (Preliminary List)
- Noel Arteche
- Bruno Cavalar
- Marco Carmosino
- Jonas Conneryd
- Tal Elbaz
- Noah Fleming
- Stefan Grosser
- Svyatoslav Gryaznov
- Dmitry Itsykson
- Raheleh Jalali
- Emil Jeřábek
- Erfan Khaniki
- Jiaqi Lu
- Christohe Marciot
- Benedikt Pago
- Shuo Pang
- Hanlin Ren
- Artur Riazanov
- Aleksandr Shekhovtsov
- Anastasia Sofronova
- Dmitry Sokolov
- Amir Tabatabai
- Neil Thapen
- Iddo Tzameret
Venue
Lecture Theatre A (LTA) & 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.
Organizers:- Marco L. Carmosino, IBM
- Ján Pich, University of Oxford
- Iddo Tzameret, Imperial College London