Episode 112, October 2026

Past the square root?

A claimed polynomial-time language that needs more than 2^A√n gates in depth-three circuits, for every constant A

Covers result 112 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 112: Past the square root? A depth-three circuit: an OR gate on top, three AND gates, six OR gates and seven input literals.

5:27. English captions available. The video loads from YouTube when you press play.

Chapters

The claims, in plain words

A depth-three Boolean circuit in the OR–AND–OR form, with unrestricted fan-in, is an OR of CNF formulas. Every Boolean function has a single CNF, so the question is size: parity, for example, needs 2ⁿ⁻¹ clauses in a CNF, each using every variable. Proving that explicit functions need large circuits is the central difficulty of complexity theory, and small depth is one of the few settings with exponential lower bounds.

Håstad’s switching lemma showed that parity needs 2^c√n gates in depth three, and Paturi, Pudlák and Zane pinned parity down to about n^1/4·2^√n, matching an upper bound. Other bounds, for majority and for a code-membership function, improved the constant in front of √n but never the square root itself; going beyond it was a recognized open problem. Much larger bounds, beyond 2^{O(n/log log n)}, would by a classical result of Valiant rule out circuits that have both linear size and logarithmic depth.

Result 112 is one OpenAI preprint (20 pages) dated September 23, 2026. It claims one language, decided by one deterministic Turing machine in polynomial time, whose n-bit membership function needs more than 2^A√n gates in any OR–AND–OR circuit, for every constant A, at all sufficiently large n. All gates are counted, bottom layer included, any fan-in is allowed, and the language is fixed before A is chosen.

What it doesn’t claim

It does not give a bound of 2^{n^1/2+ε} for a fixed ε, the question raised by Håstad, Jukna and Pudlák, and it says nothing about circuits of unbounded depth. The constants are enormous: for A = 1, the smallest test width the proof allows is 36,180.

Where it stands

Posted as a preprint: OpenAI, 20 pages, dated September 23, 2026
Peer reviewed: Not yet
Checked in Lean: OpenAI published a Lean proof of the full theorem, including the polynomial-time machine; we have not run the check

Last checked October 19, 2026. The preprint has not been revised. OpenAI published a Lean formalization, 175 files and 24,309 lines in the theorem’s import closure, including the multitape Turing machine and its running time, matched against its comparator statement, which counts every gate and allows free negations and constants; nothing outside Mathlib and Lean’s core, with no unproved steps that we could find. We have not run the check. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

The language. The input is read as blocks: data bits x, hash bits u, a monic polynomial P and coefficients β_j in F₂[Z]/(P). The data are hashed into the ring with a Hankel matrix, a polynomial with coefficients β_j is evaluated at the hash, and the input is accepted when the result’s constant coefficient is zero. The machine follows the supplied bits; it never searches for hard choices or tests irreducibility.
Counting. Fix all non-data bits to get a slice with sign g. In a circuit with S gates computing the slice, every middle gate is a CNF H whose accepted inputs are accepted by the slice, so E H = E[gH] is at most the correlation of g with H. If that correlation is tiny for every CNF of width about √n, the at most S middle gates cannot cover the slice’s accepted inputs, at least a quarter of all inputs; wider clauses are deleted at a cost of S·2^−k per gate.
A restriction lemma. Keep each variable alive with probability p and fix the others at random. A width-k CNF becomes a signed combination of CNFs of a fixed constant width b, and when p·k stays bounded the expected total weight is at most two, however many clauses the CNF has. Counting paths of successive clause violations backwards makes the number of clauses cancel; unlike Håstad’s switching lemma, the tests stay CNFs.
Hard slices. With a fixed irreducible modulus and random hash bits and coefficients, the slice’s restrictions have correlation at most 2^−|T|/8 with every width-b CNF, for most restrictions. Sunflower sparsification (Impagliazzo, Paturi, Zane) and a disjoint refinement (Dell, Husfeldt, Marx, Taslaman, Wahlén) split each narrow CNF into few sparse pieces, and hashing with polynomial interpolation gives enough independence for a moment bound over all of them. With s = 3A and the width k ≈ 3(s + 1)√(n/5), a circuit of at most 2^A√n gates would accept a vanishing fraction of inputs, a contradiction.

The numbers in the video

No clause narrower than n follows from parity for n up to 6, so a CNF for parity needs 2ⁿ⁻¹ full-width clauses.
Our implementation of the evaluator, at n = 5,000 (1,000 data bits, r = 100, t = 2), accepted 104 of 200 random inputs, about a hundredth of a second each. The Hankel hash had full rank in 300 of 300 random trials.
A toy version of a slice with 14 data bits had correlation at most 1/256 with every subcube; majority reaches 0.21.
For A = 1, the smallest constant width the proof allows is b = 36,180 (107,159 for A = 2).

Read the source

Beyond the Square-Root Exponent for Depth-Three Boolean Circuits (PDF), 20 pages.
The Lean scope note.
The collection’s catalog, where this is result 112.

The paper

OpenAI groups related papers into one result; this one has a single paper.

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

Transcript

Read the full script

0:00Depth three

A Boolean circuit of depth three, in the OR-AND-OR form studied here, with unrestricted fan-in, is an OR of ANDs of ORs: an OR of CNF formulas. Every Boolean function already has a single CNF, so depth three is about size, not possibility. A CNF can be enormous: parity, which asks whether the number of ones is odd, needs 2^(n−1) clauses, each using every variable. Proving that explicit functions need large circuits is the central difficulty of complexity theory, and small depth is one of the few settings with exponential lower bounds. In our check, no clause narrower than n follows from parity, for n up to 6. Håstad’s switching lemma showed that parity needs 2^(c√n) gates in depth three. Paturi, Pudlák and Zane pinned parity down to about n^(1/4)·2^(√n), matching an upper bound, so parity can go no further. Other bounds, for majority and a code-membership function, improved the constant in front of the square root, never the square root itself. Getting past it is a recognized open problem. Much larger depth-three bounds, beyond 2^(O(n/log log n)), would, by a classical result of Valiant, rule out circuits that have both linear size and logarithmic depth.

1:21The claim

Result 112 is one OpenAI preprint, 20 pages, dated September 23. It claims one language, decided by one deterministic Turing machine in polynomial time, whose n-bit membership function needs more than 2^(A√n) gates in any OR-AND-OR circuit, for every constant A, at all sufficiently large n. All gates are counted, bottom layer included, with any fan-in, and the language is fixed before A is chosen. The claim is weaker than 2^(n^(1/2+ε)), the question raised by Håstad, Jukna and Pudlák. The language reads its input as blocks: data bits, hash bits, a polynomial modulus, and coefficients. It hashes the data into a ring with a Hankel matrix, evaluates a polynomial there, and accepts when the result’s constant coefficient is zero. The machine just follows the supplied bits; it never searches for hard choices. In our check, our implementation of the evaluator handled 5,000-bit inputs in about a hundredth of a second each and accepted about half of random inputs. OpenAI published a Lean formalization, about 175 files and 24,000 lines, including the Turing machine. We have not run the check.

2:42How the proof goes

Suppose a circuit with S gates computes a slice of the language, with all non-data bits fixed. Each middle gate is a CNF, and every input it accepts is accepted by the top OR. If the slice’s sign has tiny correlation with every such CNF, each middle gate accepts few inputs, and S of them cannot cover the slice’s accepted inputs, about half of all inputs. So the proof needs a slice with small correlation against every CNF of width about √n; wider clauses are deleted at small cost. The main tool is a new restriction lemma. Keep each variable alive with probability p and fix the others at random. Then any width-k CNF becomes a signed combination of CNFs of a fixed constant width b. If p times k stays bounded, the expected total weight is at most two, however many clauses the CNF has. The proof counts paths of successive clause violations backwards, so the number of clauses cancels. Unlike Håstad’s switching lemma, the tests stay CNFs. Next, a hard slice. Choosing the hash bits and the coefficients at random, with a fixed irreducible modulus, gives a slice whose restrictions, with high probability, have tiny correlation with every width-b CNF. Sunflower sparsification and a disjoint refinement split each narrow CNF into few sparse pieces, and the hash with polynomial interpolation gives enough independence for a moment bound over all of them. In our check, a 14-bit toy version of the slice had correlation below 1/250 with every subcube, against about one fifth for majority. Finally, fix A, and let the width k grow like √n. Deleting the clauses wider than k changes each middle gate on at most S·2^(−k) of the inputs. If S were at most 2^(A√n), the middle gates would cover a vanishing fraction of the inputs, but the slice accepts at least a quarter: a contradiction. The constants are enormous: for A equal to one, the smallest test width b the proof allows is about 36,000.

4:56Where it stands

The preprint is not peer reviewed and has not been revised. The Lean formalization covers the full theorem, including the polynomial-time machine; we have not run it. It is not among the papers OSVerify reviewed, and we have seen no expert review. If it holds, an explicit language beats every constant multiple of √n in the exponent, at depth three; a fixed power beyond one half remains open.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.