P versus NP

P versus NP sits at the meeting point of theory and practice. It asks whether every problem whose answer can be checked quickly can also be solved quickly:

$$\text{Does } P = NP?$$

One formal way to state the distinction is:

$$P = \{p \in \mathcal{D} \mid \exists a \in \mathcal{A}: a \text{ solves } p \text{ in polynomial time}\}$$ $$NP = \{p \in \mathcal{D} \mid \exists a \in \mathcal{A}: a \text{ verifies a solution to } p \text{ in polynomial time}\}$$

where $\mathcal{D}$ is the set of decision problems and $\mathcal{A}$ is the set of algorithms.

Proof as Search

Abstractly, proof is the goal-directed application of implication rules $\mathcal{R}$ to an initial set of axioms $\mathcal{S}_0$.

1. Start with known statements $\mathcal{S}_0 = \{s_1, s_2, s_3, \dots, s_n\}$.
2. Choose an implication rule $r_i \in \mathcal{R}$.
3. Apply it to build a larger statement set:

$$\mathcal{S}_i = \mathcal{S}_{i-1} \cup r_i(\mathcal{S}_{i-1})$$

4. Stop when $\mathcal{S}_i$ contains the statement being proved.

This separates two tasks that are easy to confuse:

• proof verification: checking that each step in a proposed proof follows from the previous steps
• proof discovery: finding the right sequence of steps in the first place

Verification is local. Discovery is search.

Let $M_p$ be a proof-search machine and $M_v$ be a proof verifier. The verifier receives a finite proof trace and checks each transition. The searcher must explore the space of possible rule applications until it finds a trace that reaches the target statement.

If the proof trace has length $n$, then $M_v$ can often verify it in time polynomial in $n$. $M_p$, however, may face a branching search tree whose size grows far faster than the eventual proof.

The Temptation

It is tempting to turn this into an argument about $P$ versus $NP$:

$$\text{proofs are easy to verify} \quad \Rightarrow \quad \text{proofs are in } NP$$ $$\text{proofs are hard to find} \quad \Rightarrow \quad \text{proof search is not in } P$$

That framing is useful, but it is not yet a proof that $P \ne NP$. It shows the shape of the problem: the difference between a path and the graph that contains it. A proof is a path. Proof search is the graph traversal required to find that path.

Cook-Levin tells us that satisfiability is NP-complete, and many search problems can be encoded as satisfiability problems. If $P = NP$, then every NP-complete problem has a polynomial-time solver. That would collapse the practical distinction between finding and checking many kinds of certificates.

But the reverse move is where the argument becomes fragile. Showing that a particular proof search feels exponential, or even that a naive search is exponential, does not prove that every possible solver must be exponential.

Self-Reference

Now consider a self-referential proof attempt, call it $p_{\text{this}}$. It might aim to establish one of three claims:

$$p_{\text{this}} \Rightarrow P = NP$$ $$p_{\text{this}} \Rightarrow P \ne NP$$ $$p_{\text{this}} \Rightarrow (P = NP) \land (P \ne NP)$$

The third case is contradiction, not resolution. The first two are more subtle. A proof about proof search can become entangled with the formal system in which the proof is written.

Godel's incompleteness theorems warn that sufficiently expressive formal systems cannot, from within themselves, settle every true statement about their own consistency. That does not mean that every self-referential argument is invalid, nor does it mean that $P$ versus $NP$ is independent of our axioms. It only means that self-reference is expensive: it has to be handled with exact formal care.

What Remains

The useful part of this line of thought is the graph picture:

• an axiomatic system defines a space of reachable statements
• inference rules define edges between statements
• a proof is a path through that space
• a verifier checks a proposed path
• a prover searches for one

If $P \ne NP$, then there may be families of statements where short proofs are easy to verify but hard to discover. If $P = NP$, then a sufficiently general efficient search procedure would exist for NP certificates, with consequences far beyond theorem proving.

The unresolved question is not whether naive proof search branches. It does. The question is whether every such branch explosion can be compressed by a polynomial-time method.

Open Directions

This sketch leaves several sharper questions:

1. Can proof search be modeled as a specific NP-complete problem without smuggling in a stronger assumption?
2. Which formal systems make the proof-search graph explicit enough to study geometrically?
3. What does it mean for a statement to be independent of an axiom system in this graph view?
4. Can adding axioms be understood as adding dimensions or shortcuts to the search space?
5. What do random or evolving axiom systems look like in the limit?

That is where this attempt currently lands: not as a proof of $P = NP$, not as a proof of $P \ne NP$, but as a way to make the difference between verification and discovery feel structurally concrete.