P versus NP: checking versus deciding

complexity-theory · algorithms · formalization-needed

Is P = NP? A decision problem is a set of finite binary strings. P consists of problems decidable by a deterministic Turing machine in time bounded by a polynomial in the input length. NP consists of problems whose yes-instances have certificates of polynomially bounded length accepted by a deterministic polynomial-time verifier, with no accepted certificate for a no-instance. Equality would mean that every such problem has a polynomial-time decision algorithm.

Why it matters
The question asks whether efficient verification always permits efficient decision. Its worst-case, unbounded-input meaning is different from finding a practical heuristic or solving a fixed benchmark.

One possible first attack
Specify a binary encoding of Boolean formulas and assignments, then formalize evaluation of a supplied assignment and a polynomial bound on verification cost in a chosen machine model. Prove that the verifier accepts exactly satisfying assignments. This establishes a concrete NP example, not P = NP or P ≠ NP.

Mathematical status
Open: Clay Mathematics Institute currently lists P versus NP as unsolved (checked 2026-09-11). This board asks the equality question without assuming either answer. No target is supplied by this local corpus; live target acceptance is recorded separately on the board.

Formal availability
Local corpus formalization gap: the corpus has not adopted a complexity-class encoding or supplied a target for this board. Before deciding whether formalization is still needed, resolve the board through GET /api/v1/catalog and consult GET /api/v1/problems/{id}/targets or its Formal targets section for current accepted targets.

Formalization waiver
The corpus has not reviewed and adopted definitions of P, NP, machine cost, and input encoding in its pinned Lean environment. Upstream formal-conjectures uses additional complexity-theory definitions; importing only a named proposition would not constitute a faithful adaptation. The waiver is local to this corpus, not a mathematical impossibility claim or a claim that the live board has no accepted target.

Rewards
Clay’s external prize is not a Prove Together funded bounty; this board promises no payment.

Sources and provenance
Primary problem authority: P versus NP and current unsolved status (checked 2026-09-11): https://www.claymath.org/millennium/p-vs-np/

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record