Is finding a solution as easy as checking one? P is what a machine can decide in polynomial time; NP is what it can verify in polynomial time when handed a certificate. Down the center, a certificate goes in, the engine either checks it in a blink or searches an exponential space, and the truth comes out. The blue team builds and defends; the red team tries to fake a fast solver and gets caught.
source Cook, S. A., The Complexity of Theorem-Proving Procedures (1971), Proc. 3rd ACM STOC, 151–158 — doi.org/10.1145/800157.805047. Rendered, not quoted.
Two classes, defined by a resource bound on a Turing machine:
P — problems a machine decides in time polynomial in the input size n. NP — problems for which a short certificate exists that a machine can verify in poly time. P ⊆ NP — a decider is a verifier that simply ignores the certificate. The open question: is every verifiable problem also decidable fast?
Live cost of the current instance (from the engine):
| action | work | growth |
|---|
P vs NP is the central open question of computer science: the gap between the machine that checks a proof and the machine that finds one.
The class of checkers is defined on the-turing-machine — the same tape that decides is the one that verifies. And the-cook-levin-theorem proves SAT is NP-complete: if SAT falls to a fast decider, all of NP does. Each sphere is the next one’s premise.
The blue team’s live check: for every test instance, does the current “decider” agree with the ground truth computed by full search? If red swaps in a fake fast solver, this badge is where it shows.
Feed the machine a candidate answer — a certificate. For SAT it is a truth assignment to the variables; for CLIQUE it is a set of k vertices. The machine does not need to find it — only to check it.
| problem | certificate | verify (poly) | search (brute) |
|---|---|---|---|
| SAT | an assignment | scan L literals | 2n assignments |
| CLIQUE | k vertices | C(k,2) edges | C(n,k) subsets |
| EVEN (in P) | ignored | one mod | n/a |
A certificate is small and cheap to check. Whether one exists is the hard part — and finding it may cost an exponential search. That asymmetry is the whole question.
Everything here is computed live from the definitions — no answer is looked up. VERIFY is polynomial; SEARCH is exponential; the size of that gap is exactly what P vs NP asks.
What the machine proves, exactly, over these fixed instances: verifying a certificate is polynomial (cost = L, independent of 2n); deciding by brute force is exponential (exactly 2n assignments / C(n,k) subsets). The known answers hold: the SAT instance is satisfiable with a unique solution; a 3‑clique exists, a 4‑clique does not. And P = NP is OPEN — neither equality nor inequality is proven, and this engine claims neither.
The blue team’s witness (left) confirms these live; the red team (right) tries to fake a fast solver.
Brute force is not the only algorithm — real SAT solvers prune hard. But no one has a provably polynomial decider for any NP-complete problem, and no one has proven one is impossible. “Verify is cheap, therefore solve is cheap” is the fallacy this whole sphere is built to expose.
“P vs NP has been solved.” Cut. As of now it is open — a Clay Millennium Prize problem. This engine asserts neither P=NP nor P≠NP; the selfcheck throws if it ever did.
“NP means non-polynomial.” Cut. NP is nondeterministic polynomial — poly-time verifiable. P ⊆ NP, and P might even equal NP.
“A fast checker gives a fast solver.” Kept, corrected. Only if P = NP. The gap between checking (window 4) and searching (the grid) is the unproven part.
The red team’s move: claim to decide SAT in polynomial time — but only by checking one fixed assignment instead of searching. The blue team’s witness (window 7) is watching.
The red team pretends P=NP by “deciding” SAT in polynomial time — but only by checking a single fixed assignment instead of searching. On a satisfiable instance whose solution differs, it reports UNSAT. The witness recomputes the truth and turns red. Nothing is faked; the shortcut is real and it is caught.