we-solve (beta)

CS-156 · computer science · mathematics · Algorithmic game theory · Computational complexity

Quasilinear robust PCP for PPAD

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

An End-of-Line input $I$ consists of explicit Boolean circuits $P,S:\{0,1\}^n\to\{0,1\}^n$, with $n\ge1$, $P(0)=0$, $S(0)\ne0$, and $P(S(0))=0$. Its length $N$ counts both full circuit encodings. A solution is nonzero $v$ with $P(S(v))\ne v$ or $S(P(v))\ne v$.

A generalized circuit has finitely many nodes and a nonempty equally weighted gate list, each node the output of at most one gate. Node values lie in $[0,1]$. The gate types are constants, scaling, copying, saturated sum and difference, comparison, and Boolean OR, AND and NOT; rational gate parameters lie in $[0,1]$. Arithmetic gates have additive tolerance $\varepsilon$. Comparison sends an input gap larger than $\varepsilon$ to the corresponding output interval $[0,\varepsilon]$ or $[1-\varepsilon,1]$. Boolean gates use low inputs $\le\varepsilon$ and high inputs $\ge1-\varepsilon$, with the usual Boolean implications; absent a required implication, any output in $[0,1]$ is allowed.

Seek fixed rational $0<\varepsilon<1/10$, $0<\delta<1$, integers $A>0,b\ge0$, a polynomial $p$, and deterministic construction and decoding algorithms $R,D$. If $M$ denotes the complete output encoding length, define an acceptable witness to be a rational node assignment of binary length at most $p(M)$ satisfying at least $(1-\delta)$ of the gates. The locations of violated gates are arbitrary and every node keeps one globally consistent value. Require existence of an acceptable witness for every circuit in this model and \[ |R(I)|\le AN\lceil\log_2(N+2)\rceil^b,\qquad D(I,x)\text{ solves }I\quad\text{for every acceptable }x\text{ of }R(I). \] Construction time is polynomial in $N$; decoding time is polynomial in $N$ and the supplied witness length. The constants and algorithms are uniform, without advice or randomized construction. The encoding bound is part of acceptability, not a claim about all real assignments.

Short English statement

Can End-of-Line be reduced to robust approximate generalized circuits with quasilinear complete encoding, guaranteed polynomial-size rational witnesses, and efficient decoding of every acceptable witness?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-156-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-156

The target uses rational acceptable assignments with their polynomial encoding bound specified as part of the witness convention. The main theorem asserts their existence, a quasilinear bound on the complete circuit encoding, and deterministic decoding of every such witness even when the violated gates are chosen arbitrarily. With those exact conventions, it covers the entire search-reduction question.

Quasilinear robust PCP for PPAD

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 136; 2026-09-25), the asserted result is that End-of-Line has a deterministic quasilinear-size reduction to a generalized circuit whose approximately satisfied assignments recover a source solution despite any fixed small fraction of failed gates.

Mathematical statement of the claimed result

Manuscript 1.
An End-of-Line input contains explicit Boolean circuits $P,S:\{0,1\}^n\to\{0,1\}^n$ with $P(0)=0$, $S(0)\ne0$, $P(S(0))=0$; a solution is nonzero $v$ with $P(S(v))\ne v$ or $S(P(v))\ne v$. The claim fixes rational constants $0<\varepsilon<1/10$, $0<\delta<1$, integers $A,b$ and a polynomial $p$, and deterministic polynomial-time construction/decoding $R,D$. Its output generalized circuit has gates for constants, scaling, copying, saturated addition/subtraction, comparison and Boolean AND/OR/NOT, each node output of at most one gate. For arithmetic gates use additive error $\varepsilon$; comparison distinguishes input gaps greater than $\varepsilon$, and Boolean implications use thresholds $\varepsilon,1-\varepsilon$. An acceptable rational assignment has length at most $p(M)$ and satisfies at least $(1-\delta)$ of all equally weighted gates, with globally consistent values in $[0,1]$. \[ M=|R(I)|\le AN\lceil\log_2(N+2)\rceil^b, \qquad D(I,x)\text{ solves }I\quad\text{for every acceptable }x. \] Every generalized circuit in the model is claimed to have such an assignment. The reduction is uniform with fixed constants, counts the complete output encoding, and uses neither advice nor randomized construction; violating gates may be chosen arbitrarily.

Outline of the argument

For manuscript 1 (family 136; 2026-09-25), sparse endpoint transcripts are encoded in systematic square codes with joint-symbol robustness. Certified local programs and persistent tape equations enforce proximity, while a decreasing-disagreement correction handles commuting twists before the endpoint decoder is applied.

Formal verification

No Lean formalization is listed at this snapshot for manuscript 1 (family 136; 2026-09-25).

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →