The PCP-for-PPAD conjecture
From OpenAI Aftermath
The PCP-for-PPAD conjecture of Babichenko, Papadimitriou and Rubinstein asks for a quasilinear-size reduction from End-of-Line, the canonical complete problem of the complexity class PPAD, to generalized circuits in which both the allowed numerical error and the allowed fraction of violated gates are positive constants, with the violated gates chosen by an adversary. It is a robust, probabilistically checkable form of PPAD-hardness, and earlier work derived hardness of approximate equilibria in games and markets from it. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), listed as its result 136 and dated 25 September 2026, claims a proof of the conjecture with a reduction of size N(log N)O(1). The collection's Lean library contains the claim only as an unproved goal statement. This page summarizes the published claim and lists publicly available follow-up work.
Background
- As recounted in the introduction of the manuscript:
- PPAD and generalized circuits. Papadimitriou introduced PPAD in 1994 for total search problems whose existence proofs rest on the parity of endpoints in a directed graph; End-of-Line asks for an endpoint other than a given source of a graph described by predecessor and successor circuits. Generalized circuits, in which real values in [0, 1] on wires must approximately satisfy local arithmetic, comparison and Boolean constraints, were developed by Chen, Deng and Teng, and similar gadgets underlie the equilibrium reductions of Daskalakis, Goldberg and Papadimitriou.
- Hardness with every gate satisfied. Rubinstein proved hardness for a constant error when every gate must be satisfied, and Deligkas, Fearnley, Hollender and Melissourgos proved hardness for every error below 1/10 for the standard generalized-circuit problem with every gate satisfied. The manuscript notes that such results do not give the quasilinear size bound of the conjecture.
- The conjecture. Babichenko, Papadimitriou and Rubinstein stated the conjecture as Conjecture 2 of their 2016 paper. Rubinstein's 2016 work on two-player Nash equilibria combined encoded-path geometry, a locally evolving End-of-Line and a holographic proof system to prove quasipolynomial hardness for constant-error two-player Nash under the exponential-time hypothesis for PPAD, and left the conjecture open. Later uses also consider a weaker form, ordinary PPAD-hardness with a positive failure fraction; Golowich derives sharper two-player Nash lower bounds from PCP for PPAD together with the exponential-time hypothesis for PPAD.
The original result
- Claim. The main theorem of The PCP-for-PPAD conjecture: a quasilinear reduction states that there are fixed positive rational constants ε and δ and a deterministic polynomial-time reduction that transforms an End-of-Line instance of binary length N into a generalized circuit of total binary length N(log N)O(1), such that from any rational assignment of polynomial encoding length that ε-satisfies all but a δ fraction of the gates, whichever gates fail, a solution of the original instance can be recovered in polynomial time. Such assignments always exist, with one fixed polynomial bound on their encoding length. The size bound counts the complete output, including connection indices, auxiliary gates and the bits of all rational parameters.
- Consequences, as stated: the manuscript applies the theorem to earlier conditional reductions for weak approximate and relative bimatrix Nash equilibria, course allocation, markets with approximately optimal bundles, stationary equilibria in discounted games and approximate Hylland–Zeckhauser allocation. It states that these consequences use only the fixed-gap circuit hardness, and that the quasilinear bound is the additional assertion of the main theorem.
- Method, as described: an outer representation of the End-of-Line graph by codes whose construction uses the ternary Goldbach theorem, a fixed-generator prime-quotient expansion and an effective least-prime bound; an inner algebraic and binary gadget with a corrected scalar line test and group-theoretic inputs; replication and synchronization through expander walks with the Margulis–Gabber–Galil bound; and a geometric displacement argument that survives clipping.
- Source (openai/math repository, commit
7ef5c0c): The PCP-for-PPAD conjecture: a quasilinear reduction, dated 25 September 2026. - Formalization. The repository has no Lean scope note or Comparator challenge for result 136. Its Lean library contains a partial file,
Mesh.lean, whose header describes it as generalized-circuit smoothing, perturbation stability and rational meshes: it defines End-of-Line and generalized circuits, states the quasilinear reduction as a goal propositionQuasilinearPCPStatementand proves supporting lemmas, and it states that applying Brouwer's theorem to establish totality, as well as the reduction, its soundness, its algorithmic realization and its complexity bounds, remain unproved.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 31 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | A quasilinear PCP theorem for PPAD, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claimed quasilinear PCP theorem for PPAD: total search problems and approximate circuits, the quasilinear reduction, why approximate solutions exist, how a path is encoded as a fixed-point problem, the outer representation and inner correction, and how replication and synchronization tolerate adversarial gate failures, with interpretation and key proof steps. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_156 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap, as a partial audit, and records no issues. It states that it read and checked the definitions and main theorem, the outer composition, the inner gadget and the geometry section, re-deriving among other steps the fine-residual bound, the endpoint rounding bound, the quasilinear size count, the totality lemma and the Margulis–Gabber–Galil gap. It did not audit in depth the macrograph, outer codes, outer programs and representation, the inner algebra and binary tables, the section on games and markets and the appendix, and it notes that these supply the interfaces used as black boxes, so that any remaining gap would most likely be there. | Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-16 | AI Proved What?, episode 136 PCP for PPAD?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of the claimed proof of the quasilinear PCP-for-PPAD conjecture of Babichenko, Papadimitriou and Rubinstein: fixed constants 0 < ε < 1/10 and 0 < δ < 1 and a deterministic polynomial-time reduction from End-of-Line instances of length N to generalized circuits of length at most a constant times N times a fixed power of log N, such that from any assignment satisfying all but a δ fraction of the gates to within ε, wherever the failures fall, a decoder recovers a solution in polynomial time, and such assignments always exist. The episode states that ε, δ and the power of the logarithm are never computed, that the derived PPAD-hardness of approximate equilibria in several games and markets goes through earlier reductions that need only robustness to a constant fraction of broken gates rather than the quasilinear size, and that running-time lower bounds for equilibria still need the exponential time hypothesis for PPAD. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 147 pages, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: no, a partial Lean file states the theorem and proves only supporting lemmas. The page states that the preprint has not been revised, that there is no Lean formalization of the theorem, the partial file defining End-of-Line and generalized circuits, stating the quasilinear statement and proving only supporting lemmas, that the paper is not among those OSVerify reviewed, and that it has seen no expert review. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
