we-solve (beta)

CS-16-A2 · revision r1 · on CS-16

OpenAI claim summary for CS-16

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The lower bound is for the depth-three OR--AND--OR model with its stated gate conventions. This problem allows unrestricted binary circuits, and a depth-restricted lower bound does not give the requested general circuit separation.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Superlinear Circuit Lower Bounds for Explicit Boolean Functions
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Superlinear Circuit Lower Bounds for Explicit Boolean Functions

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 112; 2026-09-23), the asserted result is that one polynomial-time language eventually needs more than $2^{A\sqrt n}$ depth-three OR--AND--OR gates for every fixed $A$.

Mathematical statement of the claimed result

Manuscript 1.
The claim constructs one language $L\subseteq\{0,1\}^*$ decidable by a fixed deterministic Turing machine in polynomial time. For its length-$n$ Boolean function $f_n$ and minimum size $S_3(f_n)$ of circuits with three successive unbounded-fan-in layers OR--AND--OR, literal inputs and optional bottom constants, and free input negations, it asserts \[ \lim_{n\to\infty}\frac{\log_2S_3(f_n)}{\sqrt n}=\infty, \quad\text{equivalently}\quad \forall A>0\ \exists N_A\ \forall n\ge N_A:\ S_3(f_n)>2^{A\sqrt n}. \] The circuit family may be nonuniform, and there is no bound on bottom fan-in. The size counts every AND or OR gate, including gates in the bottom layer and the output gate.

Outline of the argument

For manuscript 1 (family 112; 2026-09-23), a random restriction expresses moderately wide CNFs as signed combinations of constant-width CNFs with controlled total coefficient mass. A fixed hard-slice language has low correlation with those tests, so no bounded number of middle gates can cover its positive inputs.

Formal verification

For manuscript 1 (family 112; 2026-09-23), OpenAI lists Lean statements for this assertion: one polynomial-time language eventually needs more than $2^{A\sqrt n}$ depth-three OR--AND--OR gates for every fixed $A$.

This coverage does not establish a formal proof of the complete problem as stated here.

The linked family Comparator checks are DepthThree.lean.

Their named declarations include OAI.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound.

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