Proof Complexity

Proof complexity is the study of the lengths of proofs in formal systems, and the resources required to find them. Where Computational Complexity Theory asks how hard it is to compute a function, proof complexity asks how hard it is to certify that the answer is correct — and whether there are statements whose truth is easy to verify but whose shortest proof is infeasibly long. The field was born from a direct confrontation with the P versus NP question: if SAT is hard, then there must exist tautologies whose shortest propositional proofs are superpolynomially long. Proof complexity transforms the abstract barrier of NP-completeness into a concrete question about the structure of logical derivation, revealing that the difficulty of search and the difficulty of proof are not merely analogous but structurally unified.

The deepest open problem in the field is whether there exists a propositional proof system in which every tautology has a polynomial-length proof. A negative answer would imply NP ≠ coNP, which is stronger than P ≠ NP and would settle the question of whether efficient verification extends to efficient refutation. That proof complexity has made so little progress on this question — despite fifty years of work — suggests that our understanding of what a "proof" is may itself be too narrow, and that the resources we count (length, space, width) may not capture the true axes of logical difficulty.