∑math20

Theoretical computer science · Result 112

Beyond the square-root exponent for depth-three circuits

1 paperLean

Constructs a single language in deterministic polynomial time whose n-bit membership function requires \(2^{\omega(\sqrt n)}\) total gates in unbounded-fan-in OR–AND–OR circuits, at every sufficiently large input length. This crosses the square-root-exponent threshold for explicit depth-three Boolean circuit lower bounds.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Beyond the Square-Root Exponent for Depth-Three Boolean Circuits

Beyond the Square-Root Exponent for Depth-Three Boolean Circuits

OpenAI · September 23, 2026

We construct a language in deterministic polynomial time whose n-bit membership function requires \(2^{\omega(\sqrt n)}\) gates in an unbounded-fan-in OR–AND–OR circuit. The bound holds at every sufficiently large input length and counts all gates, including the bottom layer.

Read PDF Download Source

Cite
@misc{OAI:Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026,
  author = {{OpenAI}},
  title = {{Beyond the Square-Root Exponent for Depth-Three Boolean Circuits}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026/main.pdf}{OAI:Beyond-the-Square-Root-Exponent-for-Depth-Three-Boolean-Circuits-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result gives one polynomial-time Boolean language whose exact depth-three OR–AND–OR circuit size eventually exceeds \(2^{A\sqrt n}\) for every fixed \(A>0\). The language and its polynomial-time algorithm are fixed before \(A\) is chosen, while circuits may vary with the input length. Gates have unrestricted finite fan-in and sharing, with free input negations and constants. The result does not assert a fixed exponent \(n^{1/2+\varepsilon}\) or a lower bound for unrestricted depth.

Comparator links

ResultComparator statement
Depth-three circuit lower bound beyond every square-root constantDepthThree.lean

Scope note on GitHub →