I research whether and why many fundamental computational problems require exponential time for widely used algorithms. This is studied in proof complexity through the analysis of formal deductive systems. The methods draw on combinatorics, logic, and circuit and communication complexity, with applications to combinatorial optimisation and learning theory.