p_vs_np

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

P vs NP Problem: Is $\mathsf{P} = \mathsf{NP}$? Does every problem whose solution can be efficiently verified also have an efficient solution algorithm?

Most computer scientists believe $\mathsf{P} \neq \mathsf{NP}$ but no proof exists. This is one of the 7 Millennium Prize Problems ($1M). The simplest formulation: the Boolean satisfiability problem (SAT) cannot be solved in polynomial time.

Source: Cook, S. (1971). Proc. 3rd ACM STOC. Karp, R. (1972). In: Complexity of Computer Computations. Springer. Clay Mathematics Institute.

Why this node was retired

The posted statement is

theorem p_vs_np :
    ¬∃ (p : ℕ → ℕ) (decide : List Bool → Bool),
      (∀ n, p n ≤ (n + 2) ^ 6) ∧
      (∀ (formula : List Bool), (∃ assignment : List Bool,
          assignment.length ≤ p formula.length ∧
          decide (formula ++ assignment) = true) ↔
        decide formula = true) := by
  sorry

The arbitrary Boolean function need not decide SAT and the numerical p is not a runtime bound.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Define languages and deterministic/nondeterministic polynomial-time computation and ask P=NP or P≠NP; equivalently use a sound SAT encoding and a polynomial-runtime decision algorithm with satisfiability correctness.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.