Article1 research mainline
Mapping Every Known Road to P ≠ NP: What a 13-Round Research Sprint Actually Found
This is the first of two posts about an intensive research project on the P versus NP problem. This post covers the mathematics. A companion post covers the unusual way the work was organized — as a structured collaboration between multiple large language models acting as researchers and adversarial auditors of one another.
Spoiler up front: P ≠ NP was not proved, and nothing below claims otherwise. What the project produced instead is something rarer than another failed proof attempt: a precise, cross-audited map of exactly where every currently known route to P ≠ NP is blocked, a collection of new conditional theorems and finite exact classifications, and a well-documented graveyard of refuted ideas — complete with the counterexamples that killed them.
The setup
The project was organized in four phases. Phase 1 was a complete survey of the terrain: the known circuit lower bounds, the three great barriers (relativization, natural proofs, algebrization), and a catalog of historically failed attempts. Phase 2 identified the "residual space" — the regions of proof-strategy space that the barriers do not fully exclude. Phase 3 developed and stress-tested new approaches along two main lines, alternating between theoretical reasoning and code experiments. Phase 4 formalized the surviving fragments into rigorous proof documents and a paper draft.
A core working principle was that the three barriers are treated as a map, not as enemies: each barrier tells you what a proof cannot look like, so the blank space around them is where an answer would have to live. A second principle was that failures are recorded as carefully as successes — the project maintains explicit "epitaph" files for every dead approach, on the theory that knowing precisely why something fails is the most valuable artifact a failed attempt can leave behind.
Main line A: the Williams-style algorithmic method
The first main line pursued Ryan Williams' celebrated program, which converts faster-than-brute-force satisfiability algorithms into circuit lower bounds (the technique behind NEXP ⊄ ACC⁰). The project dissected exactly where this method breaks when one tries to push it from NEXP-level statements down toward NP and P ≠ NP.
The central obstruction that emerged — nicknamed the quantifier wall — is a quantifier-exchange problem. The method naturally yields statements of the form "for every constant k there exists a hard language Lk," but P ≠ NP via non-uniform lower bounds needs "there exists a single language L hard for every k." The team proved a quantifier-equivalence theorem (∃∀ ⟺ ∃-infinitely-often) that clarifies the relationship, but also showed that the obvious extraction argument is circular, so the equivalence does not let you cross the wall.
There was genuine positive progress here. By specializing Murray–Williams to an unrestricted GAP-CIRCUIT-UNSAT problem — after two independent audits caught real errors in the first version of the argument (one confusing a fixed NTIME class with all of NP, another missing the extra time cost of a PCP oracle verifier) — the team improved a hardness-magnification exponent from j⁴ to j³ under the standard assumption. It is a sharpening of the known machinery, honestly labeled as a conditional theorem, and honestly labeled as still not connected to P ≠ NP because the quantifier wall survives.
Every other sub-route of line A ended in an epitaph: direct-padding tricks and three diagonalization strategies were shown to be circular or broken; an LP-duality certificate route was killed by showing the relaxation cannot capture the pigeonhole principle PHPn; and a "black-box compression" idea for reductions was closed with a counting counterexample. The two classical survival conditions — a superpolynomial improvement for general Circuit-SAT, or a compressing reduction beyond the direct-padding no-go — remain exactly as open as they have been for thirty years.
Main line E: proof complexity
The second main line worked in proof complexity: the study of how long formal proofs of tautologies must be, where superpolynomial lower bounds for strong systems like Frege would have deep consequences.
The technical heart was a family of results about occurrence-indexed sequent calculus (LK) proofs. The team formalized and triple-audited a signature memoization theorem (E1c): split signatures along a proof's tree unfolding can be memoized per node, giving a state bound of roughly O(Σv 2hv + ‖π‖ + |D|), where hv counts interface formula occurrences at node v. Small hand-checked counterexamples (a 4-node self-cut configuration) sharpened the statement, and later work tightened the exponent base from all occurrences to shared-only occurrences.
A striking episode was the fate of "Conjecture R," a linear-demand conjecture proposed within the project itself. One of the agents first discovered and fixed a genuine bug in its own simulation code, then constructed a "masked XOR cascade" that definitively refuted the conjecture in the abstract relation model — exponential demand growth, reproduced across random seeds. But it then showed the refuting construction cannot be realized inside standard LK, closing a "legality gate" and salvaging a restricted version of the program. This refute-your-own-conjecture-then-rescue-a-weaker-one arc is exactly what healthy research looks like, and it is fully documented.
The most developed thread, H-C9, built a certificate-carrying Lovász-theta separator: a pipeline that turns an interior-point (Newton) computation of the theta function into an explicit proof object in an extension-relative Extended Frege system. Round 13 closed this pipeline component by component — integer sum-of-squares local compilation into bounded arithmetic, exact dual-slack recovery from a single Newton trace, and typed gluing into the E1l system — each step passing independent adversarial audit. The result is a genuinely nontrivial relative-EF package.
And then it hits the third wall, which the project calls the S2 barrier: transferring the result from the extension-relative system to plain Frege requires extension elimination, which incurs an exponential blow-up. Weak systems have known lower bounds but can't carry the construction; strong systems carry the construction but have no known lower bounds. The blow-up was localized precisely — to Newton extension wires, proof duplication, and full substitution — and the remaining mass bounds are recorded as open obligations rather than papered over.
The exhaustive finite classifications
Alongside the theory, the project ran a large program of exact finite computation on monotone circuit complexity for the (5,3) threshold-type function: the exact monotone formula size is 23 gates, and the monotone DAG size was bracketed to 13 ≤ C ≤ 23 by exhaustively excluding gate counts g = 11 and g = 12. The g = 12 case alone required classifying source-use excess-3 circuits into 20 routing skeletons and 1,661 gate-allocation rows, all eliminated by complete truth-table enumeration. The g = 13 frontier was mapped into 5 profiles, 138 skeletons, and 26,521 allocation rows, with tens of thousands of rows eliminated through boundary-signature dynamic programs checking hundreds of millions of state transfers — every tranche independently reimplemented in a second language before acceptance. Whether g = 13 circuits exist remains open, and the documents say so explicitly.
The three universal walls
The project's final synthesis reduces the entire landscape to three obstructions that, between them, block every route examined:
1. The natural proofs barrier (Razborov–Rudich): combinatorial, constructive lower-bound techniques collide with pseudorandom function generators. This closes the classical circuit-lower-bound routes and, in a dual form, the LP-relaxation route.
2. The quantifier wall: Williams-style methods cannot exchange "for every k there is a hard Lk" into "one L hard for every k," and the required algorithmic improvement for general Circuit-SAT has resisted three decades of effort.
3. The S2 barrier: in proof complexity, every construction rich enough to encode the needed computation lives in a system too strong for known lower-bound techniques, and eliminating the extra strength costs exponentially.
Each of the roughly fifteen distinct routes surveyed — from GCT reformulations and Karchmer–Wigderson communication games to matrix rigidity and topological data analysis — is assigned to one of these walls, with a stated confidence of breakthrough (mostly 0.05–0.10) and a pointer to the exact open lemma that would change the assessment.
Why publish a map of failures?
Because in a problem like P versus NP, the map is the progress. The sharpened j³ magnification theorem, the E1c memoization theorem, the relative-EF closure of the certificate-carrying separator, and the exact monotone classifications are real mathematical artifacts. But the more durable contribution may be methodological: every claim in the project carries a status label (unconditional theorem, conditional theorem, conjecture, or experimental observation), every refutation carries its minimal counterexample, and every open gate is stated as a falsifiable lemma. If someone eventually walks through one of those gates, this map will tell them exactly which doors it unlocks — and which walls are still standing behind it.
The companion post describes how this was all coordinated: the ownership rules, the adversarial audit protocol, and what it looks like when five different AI systems catch — and correct — each other's mathematical mistakes.
Sources: All material in this post is drawn from the project's internal documentation: the project charter and README, the Phase 1 barrier survey (relativization, natural proofs, algebrization dossiers), the round summaries (Rounds 2–13), the final overview of open gates, the LP-limits report, the formal proof documents for E1c/H-C9, and the associated experiment logs and result files. Background results referenced therein include Razborov–Rudich (natural proofs, 1997), Williams (NEXP ⊄ ACC⁰, 2011), Murray–Williams (2018), and Haviv (2018) on minrank versus the Lovász theta function.