Conjectures in Complexity Theory

This file contains formal statements of some of the main open conjectures in complexity theory, including

• the P vs NP problem
• the NP vs coNP problem

References:

• Wikipedia
• Arora, Sanjeev, and Boaz Barak. Computational complexity: a modern approach. Cambridge University Press, 2009.
• The Clay Institute

@[reducible, inline]

abbrev ComplexityTheory.DecisionProblem : Type

The type of decision problems.

We define these as functions from lists of booleans to booleans, implictly assuming the usual encodings.

Equations

• ComplexityTheory.DecisionProblem = (List Bool → Bool)

@[reducible, inline]

abbrev ComplexityTheory.ComplexityClass : Type

The type of complexity classes. We define these as sets of decision problems.

Equations

• ComplexityTheory.ComplexityClass = Set ComplexityTheory.DecisionProblem

def ComplexityTheory.IsComputableInPolyTime {α β : Type} (ea : Computability.FinEncoding α) (eb : Computability.FinEncoding β) (f : α → β) : Prop

A simple definition to abstract the notion of a poly-time Turing machine into a predicate.

Equations

• ComplexityTheory.IsComputableInPolyTime ea eb f = Nonempty (Turing.TM2ComputableInPolyTime ea eb f)

def ComplexityTheory.P : ComplexityClass

The class P is the set of decision problems decidable in polynomial time by a deterministic Turing machine.

Equations

• ComplexityTheory.P = {L : ComplexityTheory.DecisionProblem | ComplexityTheory.IsComputableInPolyTime finEncodingListBool Computability.finEncodingBoolBool L}

def ComplexityTheory.NP : ComplexityClass

The class NP is the set of decision problems such that there exists a polynomial p over ℕ and a poly-time Turing machine where for all x, L x = true iff there exists a w of length at most p (|x|) such that the Turing machine accepts the pair (x,w).

See Definition 2.1 in Arora-Barak (2009).

Equations

• One or more equations did not get rendered due to their size.

def ComplexityTheory.coNP : ComplexityClass

The class coNP is the set of decision problems whose complements are in NP.

Equations

• ComplexityTheory.coNP = {L : ComplexityTheory.DecisionProblem | Lᶜ ∈ ComplexityTheory.NP}

theorem ComplexityTheory.P_ne_NP : P ≠ NP

P ≠ NP:

The conjecture that the complexity classes P and NP are not equal.

theorem ComplexityTheory.NP_ne_coNP : NP ≠ coNP

NP ≠ coNP:

The conjecture that the complexity classes NP and coNP are not equal.

theorem ComplexityTheory.coP_eq_P : {L : DecisionProblem | Lᶜ ∈ P} = P

The theorem that the set of complements of languages in P is itself P.

This can be proven by observing that the boolean negation function is computable in polynomial time, and that compositions of poly-time computable functions are also poly-time computable.

theorem ComplexityTheory.P_subset_NP : P ⊆ NP

The theorem that P is a subset of NP.

This can be proven by observing that for any language in P, we can construct a verifier that ignores the witness and simply runs the poly-time decider for the language.

theorem ComplexityTheory.P_subset_coNP : P ⊆ coNP

The theorem that P is a subset of coNP.