Loading field map
Proof complexity is the branch of computational complexity theory that studies the difficulty of proving mathematical statements. Where classical complexity theory asks how much time or memory a computer needs to solve a problem, proof complexity asks how long a formal proof must be, or how many symbols it must contain, when the proof is written in a particular restricted system. The subject sits at the intersection of logic, combinatorics, and algorithm design, and it has deep connections to questions about whether certain computational problems are hard.
The fundamental object of study is a proof system: a set of rules for deriving conclusions from axioms, together with a way to check that a proposed proof is valid. A proof system is sound if every statement it proves is true, and complete if every true statement has a proof. Classical logic provides complete proof systems, but completeness says nothing about how long the proof must be. Proof complexity asks: given a true statement, how long is the shortest proof of it in a given system?
The most important measure of proof length is size—the number of symbols in the proof, usually counted as a function of the length of the statement being proved. A proof system is polynomially bounded if every true statement has a proof whose size is at most a polynomial function of the statement's length. The central conjecture of the field, the NP ≠ coNP problem, is equivalent to the statement that no polynomially bounded proof system exists for all of propositional logic. This is a stronger and less studied relative of the famous P ≠ NP question. If NP ≠ coNP, then there are true statements whose shortest proofs are super-polynomially long in every reasonable proof system.
A second central question concerns the simulation order among proof systems. A proof system P simulates another system Q if every Q-proof can be translated into a P-proof with only a polynomial increase in size. If P simulates Q but not vice versa, then P is stronger: it can prove everything Q can, and sometimes much more efficiently. The field's goal is to map this hierarchy, identifying which systems are equivalent, which are incomparable, and which are strictly stronger.
The subject emerged from two distinct traditions. The first was proof theory, founded by David Hilbert and developed by Gerhard Gentzen in the 1930s. Gentzen's sequent calculus and natural deduction provided clean formal systems for mathematical reasoning, and his cut-elimination theorem showed that any proof could be transformed into one with a certain normal form. This gave a way to measure proof complexity: the cut-elimination process can blow up proof size enormously, and understanding when this blow-up is unavoidable became a central theme.
The second tradition was computational complexity theory, which took shape in the 1960s and 1970s. Stephen Cook's 1971 paper on NP-completeness explicitly connected propositional proof length to the P vs. NP question. Cook observed that if a particular proof system for propositional logic were polynomially bounded, then NP would equal coNP. This observation turned proof complexity from a branch of logic into a branch of complexity theory.
The modern field crystallized in the late 1970s and 1980s with the work of Stephen Cook and Robert Reckhow, who defined the general notion of a proof system and proved that the existence of a polynomially bounded system is equivalent to $NP = coNP$. Around the same time, researchers began studying specific systems—resolution, Frege systems, and their variants—and proving lower bounds on proof size. The first major lower bound was for resolution, a simple but widely used system, where it was shown in the 1980s that certain tautologies require exponentially long proofs. This result, due to Armin Haken, was a landmark: it gave an unconditional super-polynomial lower bound for a natural proof system.
Proof complexity is organized around a family of proof systems, each capturing a different style of reasoning. These systems are not rival schools in the sense of competing paradigms; rather, they form a spectrum from weak to strong, and much of the field's work consists of understanding the relationships among them.
Resolution is the simplest and most studied proof system. It operates on clauses—disjunctions of literals, where a literal is a variable or its negation. The only rule is the resolution rule: from two clauses (A $\lor $ x) and (B $\lor $ $\neg $x), infer (A $\lor $ B). A resolution proof of an unsatisfiable formula is a derivation of the empty clause, which represents a contradiction. Resolution is complete for refuting unsatisfiable formulas, but its proofs can be very long.
Resolution is important for two reasons. First, it is the proof system underlying most practical automated theorem provers, particularly those based on the DPLL algorithm (Davis–Putnam–Logemann–Loveland). Second, it is weak enough that strong lower bounds are known. Haken's exponential lower bound for the pigeonhole principle—the tautology stating that you cannot put n+1 pigeons into n holes—showed that resolution cannot efficiently prove even simple combinatorial facts. Subsequent work extended this to many other families of tautologies.
Variants of resolution include tree-like resolution, where each derived clause is used at most once, and regular resolution, where no variable is resolved on more than once along any path in the proof. These variants are strictly weaker than general resolution, and understanding the gaps between them has been a productive line of research.
A different family of systems represents Boolean formulas as polynomials over a field. The polynomial calculus (also called the Gröbner basis proof system) starts with polynomial equations that encode the formula's constraints and derives new equations by linear combination and multiplication by variables. A refutation is a derivation of the equation $1 = 0$, which is impossible if the original equations have a solution.
Algebraic systems are natural for proving lower bounds because they connect to algebraic geometry and commutative algebra. The degree of a proof—the maximum degree of any polynomial appearing in it—is a key measure. Lower bounds on degree can be proved using combinatorial and algebraic techniques, and these often translate into size lower bounds. The polynomial calculus is incomparable with resolution: there are tautologies that are easy for one but hard for the other.
A related system is the Nullstellensatz proof system, which is a restricted version of polynomial calculus where all polynomials are derived in a single step from the initial equations. It is weaker than polynomial calculus but easier to analyze.
Frege systems are the most general class of proof systems that resemble ordinary mathematical reasoning. A Frege system is any system with a finite set of axiom schemas and inference rules that is implicationally complete—that is, it can prove any valid implication. The precise choice of axioms and rules does not matter for complexity, because any two Frege systems simulate each other. This robustness makes Frege systems the natural benchmark for "reasonable" proof systems.
No super-polynomial lower bound is known for Frege systems. This is the central open problem of the field. The difficulty is that Frege proofs can use arbitrary formulas as intermediate steps, and they can reuse derived formulas many times. This flexibility seems to give them enormous power, and all known lower-bound techniques fail against them.
Between resolution and full Frege systems lies a hierarchy of restricted Frege systems. The most important are:
The hierarchy of Frege systems mirrors the hierarchy of circuit complexity classes, and lower bounds for proof systems often follow from lower bounds for the corresponding circuit classes. This connection is one of the field's most powerful tools.
Gentzen's sequent calculus provides a framework that unifies many proof systems. A sequent is a statement of the form Γ ⊢ Δ, meaning that the conjunction of formulas in Γ implies the disjunction of formulas in Δ. The calculus has rules for introducing each logical connective on the left and right, plus the cut rule, which is a generalized modus ponens.
The cut rule is the only rule that removes information: it allows you to combine a proof of Γ ⊢ Δ, A with a proof of Γ, A ⊢ Δ to get a proof of Γ ⊢ Δ. Cut-elimination shows that any proof can be transformed into one without cuts, but the transformation can increase proof size exponentially. Proof complexity studies the minimum cut-free proof size, and the gap between proofs with and without cuts is a measure of the system's strength.
The sequent calculus is particularly important for bounded arithmetic, a family of weak theories of arithmetic that correspond to the polynomial hierarchy. These theories are used to formalize reasoning about polynomial-time computable functions, and their proof complexity is intimately connected to the complexity of the functions they can define.
Bounded arithmetic is the study of weak fragments of Peano arithmetic where induction is restricted to formulas of bounded quantifier complexity. The most famous of these is S₂¹, which corresponds to polynomial-time computable functions. The connection to proof complexity comes through the witnessing problem: if a bounded arithmetic theory proves a statement of the form "for every x there exists y such that P(x,y)", then there must be a polynomial-time function that computes such a y. This is a witnessing theorem, and it shows that the proof strength of a theory is tied to the computational power of the functions it can define.
Bounded arithmetic provides a bridge between propositional proof complexity and first-order logic. The translation of a first-order formula into a family of propositional formulas—the Paris–Wilkie translation—turns statements about the strength of theories into statements about the lengths of propositional proofs. This translation is a key tool for transferring lower bounds from propositional proof systems to theories of arithmetic, and vice versa.
The field today is characterized by a rich web of connections among proof systems, circuit complexity, and computational hardness. Several themes dominate current research.
The known lower bounds for weak proof systems fall into a few families. For resolution, the main technique is the width method, which shows that a proof of small size must contain a clause of small width (number of literals), and then proves that certain formulas require large width. This technique, developed by Ben-Sasson and Wigderson, gives near-optimal lower bounds for many formulas.
For algebraic systems, lower bounds often come from degree lower bounds proved via combinatorial or algebraic arguments. The functional pigeonhole principle and related combinatorial principles are the standard hard examples.
For bounded-depth Frege systems, the main technique is random restrictions, borrowed from circuit complexity. By randomly fixing some variables, one can simplify the proof structure and show that any proof must be large. This technique has been refined over decades and remains the only known method for these systems.
The central open problem is to prove super-polynomial lower bounds for Frege systems or for the polynomial calculus with resolution (a combined system that is stronger than either alone). All known techniques fail for these systems, and there is a sense that fundamentally new ideas are needed. Some researchers believe that such lower bounds are beyond current mathematics, while others point to connections with circuit lower bounds as a possible route.
A related question is whether there exists a super proof system—one that simulates all others. The optimal proof system conjecture asks whether there is a single system that is essentially as strong as any other. This is equivalent to a statement about the structure of the polynomial hierarchy, and it remains open.
Proof complexity has practical implications for SAT solving, the problem of determining whether a Boolean formula is satisfiable. Modern SAT solvers are based on the DPLL algorithm with clause learning, which corresponds to a proof system called resolution with clause learning. Understanding the limits of this system—what kinds of formulas are hard for it—has direct consequences for the performance of SAT solvers. The field has produced a rich theory of proof systems for SAT, including the DRAT system used in the most successful solvers, and the question of whether these systems can be polynomially bounded is actively studied.
Two additional techniques deserve mention. Feasible interpolation is a method for proving lower bounds by showing that a proof system can be used to extract a small circuit that separates two sets. If no such small circuit exists, then the proof system must be weak. This technique has been used to prove lower bounds for resolution and for some algebraic systems, and it connects proof complexity to circuit complexity in a direct way.
Randomized proof systems allow proofs to use randomness, and the question of whether randomness helps is studied in the context of probabilistically checkable proofs (PCPs). PCPs are central to modern hardness of approximation results, and their study has influenced proof complexity by introducing new measures of proof efficiency.
Proof complexity is a mature field with a clear structure. Its core objects—resolution, algebraic systems, Frege systems, and bounded arithmetic—are well understood in their relationships, even though the central lower-bound questions remain open. The field's methods are drawn from logic, combinatorics, and circuit complexity, and its results have implications for automated reasoning, SAT solving, and the foundations of mathematics.
The most important unresolved questions are the existence of super-polynomial lower bounds for Frege systems and the related question of whether $NP = coNP$. These questions are widely believed to have negative answers, but no proof is known. The field's progress has been steady but slow, with each new lower bound extending the frontier to slightly stronger systems. The hope is that a breakthrough on Frege systems would not only resolve a central question in complexity theory but also illuminate the nature of mathematical proof itself.