P versus NP
Lax434930.PVersusNP · concepts/Lax434930/PVersusNP.lean · lax-434930
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural 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 as an open question.
Concept map
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
| 1 | import Lax434930.PolynomialTime |
| 2 | import Lax434930.NondeterministicPolynomialTime |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: P versus NP |
| 7 | type: open question |
| 8 | --- |
| 9 | The P versus NP problem asks whether every language with polynomially |
| 10 | bounded, polynomial-time verifiable certificates can also be decided in |
| 11 | deterministic polynomial time. We state the conjectured separation |
| 12 | as an open question. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax434930.PVersusNP |
| 16 | |
| 17 | open PolynomialTime NondeterministicPolynomialTime |
| 18 | |
| 19 | /-- The conjectured separation of P and NP, left as an open question. -/ |
| 20 | axiom P_ne_NP : P ≠ NP |
| 21 | |
| 22 | end Lax434930.PVersusNP |
| 23 |
Used by
none
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments