Efficient proofs and computations: a unifying approach

Computational complexity developed greatly since the 1970s and now spans all aspects of efficient computation from analysing concrete applied problems to some of the deepest mathematical questions raised in the 20th century.

The most famous of these is one of the Millennium Problems known as the P versus NP problem.Many of the central questions regard understanding the resources required to solve problems.

For example, in circuit complexity we ask: given a computational task f—e.g., adding two numbers—what is the minimum number of logic gates that any circuit must use to solve f?

And in proof complexity: given a tautology T—e.g., T could encode the correctness of an algorithm—what is the minimum size of a formal proof of T?Exciting new, and unexpected, connections between circuits and proofs have had a transformative impact in both circuit and proof complexity. Some of these appeared already in the late 90s, but the last six years has seen an impressive revival.

There are many reasons to believe that we have only scratched the surface of a promising technique that will yield important insights on existing open problems.My aim is to study computational problems with emphasis on these connections.

I hope to develop mathematical methods that can provide in-depth theoretical understanding of the basis for efficient computations, and that these insights will lead to more powerful, and provably correct, algorithms for computational problems that are currently out of reach.