Shuo Pang: Homepage

s.(last name)@bristol.ac.uk

Hi, I am a lecturer in computer science at the University of Bristol.

I work in computational complexity and discrete mathematics, broadly on the limits of efficient computation.

My focus is on proof complexity, which studies what can or cannot be efficiently proved. There is a simple computation–proof connection: the 'whys' behind each computation step, when formalized and chained together, is a proof that justifies the output. If moreover the computation is efficient, the proof is expected to be short.

Here is an example: given a graph that's not 3-colourable, how hard is it to prove this fact? Can it always be proved in \(|G|^{10}\) steps in ZFC? If \(G\) avoids all "easy evidence" like having a 4-clique, or is a very sparse random graph, then intuition may suggest that every proof needs to brute force some exponential set of potential colourings.* Yet a rigorous argument remains beyond reach.

  1. * Interestingly, if the random graph model has average degree ≥ 15, short proofs do exist in simple semi-algebraic proof systems via the Lovasz-theta function. For sparser models, short proofs are unknown.

A more realistic goal is showing no short proof exists in restricted formal systems. Despite "restricted", many such systems (resolution, Gröbner bases, cutting planes, sum-of-squares, etc.) capture powerful methods in combinatorial optimisation and automated reasoning. Understanding their strength and limitations matters.

The techniques involved have a distinctive flavour, but they are well-connected to several branches in math and tcs. See more

Research Papers