Connecting Proofs and Algorithms
Par
Noah Fleming
Memorial University
Mardi 18 mars 2025, 10:30-11:30 EST, Salle 6214
Pavillon André-Aisenstadt, Université de Montréal, 2920 Chemin de la Tour
Abstract: Over the past several decades an exciting interplay has emerged between algorithms and the provability of mathematical statements, whereby short proofs give rise to efficient algorithms and vice versa. This has led to state-of-the-art algorithms for many NP-hard problems. As well, it has enabled proof complexity — the study of what can be proven efficiently — to become a powerful tool for analyzing algorithms in both theory and practice. This has resulted in provable guarantees for a large number of important classes of practical algorithms including SAT solvers, integer programming solvers, and certain convex programs. These connections have also had an outsized impact on proof complexity, with tools from algorithms resolving a large number of important open questions in this area.
In this talk I will survey this interplay and present a unifying framework for much of it. I will describe how my co-authors and I have used it in order to resolve important open problems in a wide variety of areas; these include:
- Guarantees on the runtime of state-of-the-art algorithms for solving integer programming problems,
- Trade offs between the runtime and parallelizability of a variety of algorithms,
- Separations between complexity classes
This talk is aimed at a broad computer science audience, and only a basic familiarity with complexity theory (P, NP, etc.) will be assumed.
Bio: Noah Fleming is an assistant professor at Memorial University. His research is in the area of computational complexity theory which aims to understand the nature of computation — in particular, the amount of computational resources (time, space, etc.) needed in order to solve computational problems. His particular research focus is on the complexity of proving theorems, boolean circuits, search problems, and the connections between them. He also maintains an interest in the design and analysis of robust algorithms including property testers — those which try to determine properties of massive datasets while observing only a tiny portion of them. Prior to taking a position at Memorial University, he was a postdoctoral researcher at UCSD, a research fellow at the Simons Institute, and he completed his PhD at the University of Toronto.
