Proof complexity of circuit lower bounds

One of the most fundamental and notorious open problems in theoretical computer science is the possible existence of highly efficient algorithms solving NP problems: there might be fast algorithms breaking established cryptosystems, automating theorem proving, making contemporary approaches to AI obsolete, and solving practically every computational task. This issue lies at the heart of the P versus NP problem, a central question of computational complexity, and particularly in the investigation of lower bounds on the efficiency of concrete computational models such as Boolean circuits.The notorious difficulty of proving complexity lower bounds became evident already in the early days of the theory of computing when the theory of formal barriers explaining their difficulty started to emerge. In recent years, there has been a dramatic rise of barrier results driving the field forward and connecting it to areas such as learning theory and cryptography. A better understanding of formal barriers is emerging today as the necessary requirement for further progress on central problems in computational complexity, and the goal of this project is to develop a systematic theory around it: proof complexity of circuit lower bounds. In particular, the project will bridge the rich tradition of concrete combinatorial methods with the new meta-mathematical approach via the phenomena of hardness magnification that connect strong and weak computational models. It will focus on a logic-oriented area of proof complexity investigating the lengths of propositional proofs and use its meta-mathematical perspective to explore the potential of lower bound methods in circuit complexity but also in proof complexity itself.The proposed meta-mathematical approach presents a novel perspective on established topics in computational complexity with a potential to deliver a paradigmatic shift in the field and bring us closer to the full understanding of the power of computing.