Every time you log into a bank account, send an encrypted message, or run a software verification tool, you are betting that certain computational problems are genuinely hard to solve—and this project aims to understand which problems are truly difficult and why. At its core, the research tackles the famous P vs NP question: can every problem with a quickly checkable answer also be solved quickly? Despite decades of work, progress has been agonisingly slow, and no one fully understands why the question is so stubborn. The project weaves together three promising but separate approaches—algebraic complexity, proof complexity, and meta-complexity—to build a unified picture of computational hardness. This is fundamental science with no immediate practical application. However, a deeper understanding of why certain problems resist efficient solution would underpin secure cryptography, enable faster verification of software and hardware, and improve machine learning and optimisation algorithms. Past work in this area has quietly shaped everything from internet security to airline scheduling. If successful, this project could reveal the mathematical structure that governs what computers can and cannot do—a question that touches every system that relies on computation.
View original technical description
The suggested proposal will investigate fundamental questions in computational complexity that lie at the heart of the theory of computing. The ultimate goal is to better understand which problems can be solved efficiently and which cannot. While obtaining faster algorithms is important to make progress in domains such as verification, machine learning and optimization, ruling out the possibility to quickly solve various problems underlie secure cryptography and derandomization of probabilistic algorithms. Moreover, these questions reveal deep mathematical and natural phenomena that permeate many areas of science. The central question in complexity theory is the P vs NP question, which asks whether all computational problems with efficiently verifiable solutions can also be solved efficiently. This and related questions are called lower bound questions, in which one seeks to bound from below the computational resources that are required to solve certain problems, or certain classes of problems in a given computational model, and thus showing these problems to be hard. Despite many decades of effort, progress is very slow, nor is it fully understood why the question is so hard. Relevant to this project are three quite disparate approaches to the fundamental problems in complexity theory that have grown fast in recent years along significant breakthroughs: algebraic complexity, proof complexity and meta-complexity. Algebraic complexity centres predominantly around the algebraic analogue of the P vs NP question - the VP vs VNP question asking whether the permanent is computable by small algebraic circuits. Proof complexity is a very different approach to the fundamental questions of complexity: here we consider proofs rather than computations. Cook and Reckhow showed that NP ?= P would follow if no propositional proof system is polynomially bounded (a polynomially bounded proof system can establish every sequence of tautologies with proofs of polynomial-size). Meta-complexity on the other hand is a line of research that investigates the role of self-reference in proving lower bounds, and in delineating the line between lower bounds that we can hope to achieve and those we cannot, with different types of argument. Certain recent developments have highlighted the benefit of meta-complexity hence contributing to it gaining a lot of interest. The main objective of the project is to integrate and build on recent advances in the above three approaches to flesh out a new structure within the complexity of proofs and algebraic computation. We plan to establish new proof-size and algebraic-computation lower bounds against strong (algebraic and Boolean) proof systems and algebraic circuit classes. On the flip side, by employing the meta-complexity approach, we plan to uncover formal barriers by demonstrating that a large set of methods cannot establish strong lower bounds; namely, ruling out a large class of "natural" arguments from being able to settle VP vs VNP, based on a widely-believed hypothesis that some natural family of polynomials are themselves hard—where a lower bound argument is said to be natural if the property of the object (function or polynomial) used to exhibit the hardness of the object is decidable in itself by small algebraic circuits (via the notion of natural algebraic proofs). Lastly, using both lower bounds results and the notion of formal barriers we set to introduce and study the circuit minimization problem in the algebraic setting and its applications to learning (namely, "reconstruction") of algebraic circuits.
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know