P versus NP

Lax434930.PVersusNP · concepts/Lax434930/PVersusNP.lean · lax-434930

open

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Open question

    The P versus NP problem asks whether every language with polynomially bounded, polynomial-time verifiable certificates can also be decided in deterministic polynomial time. We state the conjectured separation PNP\mathrm{P} \ne \mathrm{NP} as an open question.

    Concept map
    4 concepts
    100%
    Proven claimOpen claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax434930.PolynomialTime
    2import Lax434930.NondeterministicPolynomialTime
    3
    4/-!
    5---
    6title: P versus NP
    7type: open question
    8---
    9The P versus NP problem asks whether every language with polynomially
    10bounded, polynomial-time verifiable certificates can also be decided in
    11deterministic polynomial time. We state the conjectured separation
    12PNP\mathrm{P} \ne \mathrm{NP} as an open question.
    13-/
    14
    15namespace Lax434930.PVersusNP
    16
    17open PolynomialTime NondeterministicPolynomialTime
    18
    19/-- The conjectured separation of P and NP, left as an open question. -/
    20axiom P_ne_NP : PNP
    21
    22end Lax434930.PVersusNP
    23

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…