
Hi, I am a lecturer in computer science at the University of Bristol.
I work in computational complexity and discrete math, focusing on lower bounds in proof complexity.
Here's a typical question I like exploring: given a graph \(G\) that has no proper vertex 3-coloring, can this fact be proved in \(|G|^{10}\) steps? For an arbitrary such graph \(G\), intuition might suggest that some form of brute-force search over exponentially many potential colorings is inevitable, yet a rigorous proof remains beyond reach.
A more realistic goal is to show that short proofs don't exist in restricted (nondeterministic) formal systems. Many of these systems capture the reasoning behind widely used algorithms, so understanding their efficiency matters in theory and practice. The techniques involved have a distinctive flavour, but they also connect closely to several branches in math and TCS. See more