Definition
P not equals NP
The statement
asserts that some decision problem in NP does not belong to P: In other words, some decision problem has polynomial-length certificates for its yes-instances verifiable in deterministic polynomial time, but no deterministic polynomial-time algorithm solves it. Since
is known, this would make the inclusion strict. This is an unproved conjecture, not a theorem. Its negation is P = NP.