I am interested in the interactions between mathematical logic and complexity theory. The fundamental question underlying directly or indirectly most of my research is this:

• What is the nature of proof complexity?

In particular, what are the intrinsic reasons that some (propositional) formulas are hard to prove? Can the proof complexity of some formulas be traced to the computational complexity of associated computational tasks? Which mathematical structures relate to the existence of feasible proofs?

These questions have many technical mathematical facets, the fundamental one being the NP vs. coNP problem. I approach this topic primarily from the mathematical logic perspective which lead me to some new theorems, concepts and problems that contributed to the development of proof complexity. In particular, the concept of feasible interpolation uncovered a link between the hardness to compute and the hardness to prove, provided a versatile lower bound method and fostered unexpected connections of proof complexity with other fields (e.g. circuit complexity theory, foundations of cryptography, automated theorem proving, model checking or cellular automata).