we-solve (beta)

CS-132 · computer science · mathematics · Computational complexity

Explicit super-square-root-exponential depth-three circuits

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Is there a language in deterministic polynomial time whose n-variable membership functions require depth-three OR–AND–OR Boolean circuits of size $>2^{A\surd n}$ for every fixed $A>0$ and every sufficiently large n, with unrestricted bottom fan-in and no circuit uniformity condition?

Short English statement

Is there a language in deterministic polynomial time whose n-variable membership functions require depth-three OR–AND–OR Boolean circuits of size $>2^{A\surd n}$ for every fixed $A>0$ and every sufficiently large n, with unrestricted bottom fan-in and no circuit uniformity condition?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for CS-132

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 112; 2026-09-23).

Explicit super-square-root-exponential depth-three circuits

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$.

The selected statement includes the clause used for this problem.

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

Go to contribution →