The problem
When checking a proposed solution is easy, is there always an equally manageable way to certify that no solution exists? Consider two switches, x and y, each either on or off. Require at least one to be on and require y to be on whenever x is on. Setting y on satisfies both rules, so that setting certifies “yes.” But a failed setting cannot certify “no”: another setting might work. NP versus coNP asks whether every problem with short, quickly checkable evidence for yes also has such evidence for no.[1] [3]
The underlying question is whether efficiently verifiable yes answers and no answers always have equally expressive certificate systems. For satisfiability, a yes certificate is one assignment making a Boolean formula true. For instance, “x or y, and not x or y” is satisfied when y is true; “x and not x” is unsatisfiable. These examples illustrate the two kinds of evidence, not a separation of complexity classes. A language is a set of encoded inputs with answer yes. It is in when membership has certificates of polynomial length checked by a deterministic polynomial-time algorithm; its complement reverses yes and no. The question is , where contains complements of NP languages.[1] [3]
Scope
For ordinary unrelativized decision languages, is NP=coNP, where coNP consists of complements of languages in NP? Certificates have polynomial length and deterministic polynomial-time verification.
What remains open
It is unknown whether every NP problem also has short certificates for no answers.[2] [3]
To establish , one must rule out every polynomially bounded, efficiently checkable certificate method for some complement of an NP language. The cited 2026 algebraic result proves lower bounds for a specified restricted proof system; it does not exclude all methods. Conversely, showing an easy contradiction has a short proof says nothing about a uniform bound for every unsatisfiable formula.[2] [3]
Why it matters
An impossible set of requirements can be just as important to recognize as a workable one. The question asks whether impossibility always has compact evidence that somebody else can check, instead of having to inspect every candidate. Such evidence need not be easy to find: the issue is whether it exists. The answer would reveal whether efficient justification treats success and failure symmetrically.[1] [2] [3]
Boolean tautologies are formulas true under every assignment; negating an unsatisfiable formula gives a tautology. A sound, complete propositional proof system with proofs bounded by a polynomial in formula length exists exactly when . This turns an abstract question about complements into a question about the size of formal mathematical explanations. It also separates two resources: a short proof can be checked efficiently even when discovering that proof is expensive.[1] [2] [3]
Definitions
3 terms
certificate
A finite piece of evidence that a verifier can check against an input. NP requires an appropriate certificate for every yes input, with length and checking time bounded by fixed powers of input length.[3]
coNP
The class of complements of NP decision problems. Equivalently, a problem is in coNP when its no answers have polynomial-length certificates checked in deterministic polynomial time.[3]
tautology
A Boolean formula that is true for every assignment of on/off values to its variables.[3]
Sources
- The relative efficiency of propositional proof systems
Notes on The relative efficiency of propositional proof systems
1979 foundational article, with a separately dated 2014 online landing. The fresh publisher read exposes an extract on proof lengths and proof-system comparisons; full article access was not available. Certificate definitions and the proof-complexity connection are also supported by the added author-hosted textbook draft and the selected 2026 report introduction.
- Hard CNF Instances for Ideal Proof Systems
Notes on Hard CNF Instances for Ideal Proof Systems
Selected report introduction distinguishes polynomial-size refutations for all unsatisfiable formulas from lower bounds for restricted algebraic systems. Its new CNF lower bounds concern specified read-once oblivious algebraic branching program fragments. The landing distinguishes May 5 report submission from May 10 publication.
- Computational Complexity: A Modern Approach (January 2007 Internet draft)
Notes on Computational Complexity: A Modern Approach (January 2007 Internet draft)
Selected Chapter 2 certificate/coNP definitions and Chapter 21 proof-complexity statement. January 2007 Internet draft, not the final 2009 edition; extracted bars and class subscripts are imperfect, so the complement definitions are cross-checked against the prose and the 2026 report.