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 \(G\) that is not 3-colourable, how hard is it to prove this fact? Is there always a proof within \(|G|^{10}\) steps in ZFC? Intuition may suggest that there can be some graph which is non-3-colourable but which avoids all those "easy evidence" like the containment of a 4-clique, as sparse random graphs do, and for such graphs every proof has to brute force some exponential family of partial colourings*. A rigorous argument, however, remains beyond reach.

  1. *Interestingly, when the random graph model is regular with degree ≥ 15, short proofs do exist in simple semi-algebraic proof systems via the Lovasz-theta function (Atserias–Ochremiak, Banks–Kleinberg–Moore). 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