Proof complexity and circuit complexity: a unified approach

Can we automate creative and challenging tasks such as proving mathematical theorems or designing learning algorithms? Such questions can be formalised in the language of computational complexity theory and constitute some of the most fundamental scientific problems of our times. A famous obstacle in the centre of these pursuits, known as the P versus NP problem, asks whether it is possible to solve efficiently all problems whose solutions can be efficiently verified. A positive answer to the question would single-handedly resolve a myriad of major problems including theorem-proving and algorithm-design. 

Unfortunately, the P versus NP problem has resisted solution for over 50 years. In fact, it is consistent with our current knowledge that almost all problems in practice are solvable extremely efficiently with very small computational devices. The decades of research have led to two prominent but contrasting perspectives on the problem: the meta-mathematical view manifested in the theory of complexity of proofs (proof complexity) and a concrete combinatorial view dominant in the analysis of computational models such as logical circuits (circuit complexity). 

This project focuses on bridging these approaches. It will build on the emerging theory of hardness magnification and a rise of related new connections between logic, learning theory and cryptography. It thus has the potential to bring us closer to a full understanding of the power of computation and logical reasoning.