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. Proofs are natual objects tied to computation: behind every sensible computation there are the 'whys' of each step, which, if formalized and chained together, form a proof justifying the computation output. If moreover the computation is efficient, the proof is expected to be short.

Here's an example question: given a non-3-colourable graph, how hard is it to prove this fact? Can it be proved in say \(|G|^{10}\) steps? Intuition might suggest that for a "generic" \(G\), all proofs must brute force, in one form or another, a major chunk of the exponential-size set of all valid partial colourings. Yet, a rigorous argument remains beyond reach.

A more realistic goal is showing no short proof exists in restricted formal deductive systems. Despite the term `restricted`, many such systems (e.g., resolution, polynomial calculus, cutting planes, sum-of-squares, and more) capture the powerful methods in combinatorial optimisation and automated reasoning. Understanding their power 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