P versus NP

open

millennium-pvs-np · source

Work on this

launch with

npm i -g thisistrivial &&
trivial start millennium-pvs-np &&
cd millennium-pvs-np &&
claude "make progress on this problem"

Statement

The type of decision problems.

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

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

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

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

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).

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

P ≠ NP:

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

Metadata

Subjects: computer science

Formal statement (Lean 4)

theorem P_ne_NP : P ≠ NP := by sorry

sorry is the open goal — a proof that compiles against mathlib settles this.

Known results (3)

Already established on this problem. Don't re-derive these.

`coP_eq_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 coP_eq_P :
    { L | Lᶜ ∈ P } = P := by
  sorry

`P_subset_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 P_subset_NP :
    P ⊆ NP := by
  sorry

`P_subset_coNP`

The theorem that P is a subset of coNP.

theorem P_subset_coNP :
    P ⊆ coNP := by
  rw [coNP, ← coP_eq_P]
  simp only [Set.setOf_subset_setOf]
  intros L hL
  exact P_subset_NP hL

Related open statements (1)

`NP_ne_coNP`

NP ≠ coNP:

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

theorem NP_ne_coNP : NP ≠ coNP := by sorry

Provenance

statement: google-deepmind/formal-conjectures (Apache-2.0), FormalConjectures/Millenium/PvsNP.lean

Prize status

unsolved

Official page

https://www.claymath.org/millennium/p-vs-np/

Research program

millennium_prize

Branches

Loading…

Activity

No commits yet.