---
tag: 1Q046J0AW2
kind: concept
name: Proof complexity
msc: ["03F20", "68Q17"]
uses: [N4EDJNMTEF, 09K9MWD2QQ, 05006AJ7DZ]
sources:
  - url: https://en.wikipedia.org/wiki/Proof_complexity
same_as:
  wikidata: Q7249999
  wikipedia: Proof complexity
---

## Summary

Proof complexity is the part of [[proof theory|N4EDJNMTEF]] and of computational complexity that studies the size of formal proofs.
Its main objects are proof systems for [[propositional logic|09K9MWD2QQ]], and the question is how short a proof of a given [[tautology|05006AJ7DZ]] can be.
Cook and Reckhow showed in 1979 that a proof system with short proofs of all tautologies exists if and only if NP equals coNP.
So lower bounds on proof size for ever stronger systems are a route toward separating complexity classes.

## Explanations

### L1 human

A tautology is a formula that is true under every truth assignment.
One can check this with a truth table, but the table for $n$ variables has $2^n$ rows.
A proof can be much shorter, but it is not clear that a short proof always exists.
Proof complexity asks how long the shortest proof must be, in a given proof system.
For example, in the resolution system, every proof of the pigeonhole principle, "$n + 1$ pigeons do not fit in $n$ holes one per hole", has size exponential in $n$.