Proof Complexity

Proof complexity studies the lengths of proofs in formal systems and the computational resources required to find them. A proof system is polynomially bounded if every tautology has a proof whose length is polynomial in the size of the tautology. The central question, analogous to the P vs NP problem, is whether such a system exists — or equivalently, whether NP equals co-NP.

If NP ≠ co-NP, then every proof system for propositional logic requires superpolynomial proof length for some family of tautologies. This would mean that mathematical truth and mathematical proof are separated by a complexity gap: some truths are inherently hard to establish, regardless of the formal system used. The field studies specific proof systems — resolution, Frege, extended Frege, cutting planes — and establishes lower bounds on proof length for concrete tautology families.

Proof complexity connects computational complexity to the philosophy of mathematics: it makes precise the intuition that some theorems are deep not merely in a metaphorical sense but in a provable computational sense. The lengths of proofs in a system determine what that system can efficiently explain, just as circuit size determines what hardware can efficiently compute.

The dream of a universal automated theorem prover rests on the assumption that proof is not much harder than truth. Proof complexity suggests this dream is built on sand: if NP ≠ co-NP, then there are mathematical facts whose shortest proofs are exponentially longer than the facts themselves. Understanding is not merely slow; it may be structurally impossible to compress into feasible form. The universe of mathematics has dark corners where no lamp, however bright, can reach in polynomial time.