Depth-three circuit lower bounds beyond the square-root exponent

Depth-three circuit lower bounds beyond the square-root exponent concern explicit Boolean functions that require OR–AND–OR circuits, and more generally constant-depth AND/OR circuits, of size larger than the classical bounds coming from parity. For depth three, Håstad's switching lemma gives size 2^Ω(√n) for parity, and every known explicit lower bound stayed at a constant times √n in the exponent. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a polynomial-time language whose depth-three circuit size exceeds 2^A√n for every constant A, with a Lean formalization of the main theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • Håstad's random-restriction and switching method gives the 2^Ω(√n) depth-three lower bound for parity. Håstad, Jukna and Pudlák developed a top-down approach and improved the constants for parity and majority, and Paturi, Pudlák and Zane obtained the sharp parity bound through their satisfiability coding lemma, so parity itself cannot exceed the square-root scale. Paturi, Pudlák, Saks and Zane obtained a code-membership bound with leading exponent (π/√6)√n.
  • The question of an unbounded ratio of the exponent to √n is discussed by Gurumukhani, Paturi, Pudlák, Saks and Talebanfard and identified as open in later work; it is weaker than a lower bound 2^n1/2+ε, a question raised by Håstad, Jukna and Pudlák. For bounded bottom fan-in, Paturi, Saks and Zane, and Gurumukhani and coauthors, obtained much larger bounds in different models.

The original result

• Claim. Theorem 1.1 of Beyond the Square-Root Exponent for Depth-Three Boolean Circuits states that there is a language decided by a deterministic polynomial-time Turing machine whose n-bit membership function f_n satisfies log₂ S₃(f_n)/√n → ∞, where S₃ is the minimum total number of gates in an OR–AND–OR circuit with unrestricted fan-in and free input negations. No uniformity or bottom fan-in restriction is imposed on the circuits.
• Method, as described: a random restriction expresses each restricted wide CNF as a finite signed combination of CNFs of constant width with controlled total coefficient mass; the constructed function has small correlation with every such CNF, which forces each middle gate of an exact circuit to accept few inputs and contradicts the function's acceptance density.
• Sources. The manuscript Beyond the Square-Root Exponent for Depth-Three Boolean Circuits at commit 1581d4c.
• Formalization, as described by the repository. The scope note states that the formalized result gives one polynomial-time language whose exact depth-three circuit size eventually exceeds 2^A√n for every fixed A > 0, with the language and its algorithm fixed before A is chosen, and that it asserts neither a fixed exponent n^1/2+ε nor a bound for unrestricted depth. The Comparator statement is DepthThree.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 21 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statement)	Rates the family "full", with no note; lists the hand-written polynomial-time machine model and circuit encoding among the definitions to check, and records a sandboxed Comparator pass for DepthThree.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10	cert-machine, openai/math lane K: run 38051470892	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the DepthThree solution, in 436 s.	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list DepthThree, so it was accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	N. Chukhin, Breaking the Parity Barrier for Constant-Depth Circuits (ECCC TR26-248)	Extension (every constant depth)	For every fixed d ≥ 3, every depth-d circuit computing the trilinear function Σ ai+jxiyj mod 2 requires 2Ω((n log n/log log n)1/(d−1)) gates. The abstract states that the proof combines the restriction lemma of OpenAI, with a short new proof, with Håstad's switching lemma and the sparsification lemma of Calabro, Impagliazzo and Paturi.	ECCC report, published 11 October 2026.
2026-10-21 (listed)	X. Li, Y. Zhong, Short Point Lists for CNFs and Stronger Constant-Depth Circuit Hardness (arXiv:2610.27127)	Extension (improved bounds)	Decomposes every bounded-width CNF into at most 2εm width-b CNFs each determined by few satisfying assignments, and proves for every fixed d ≥ 3 a size lower bound 2Ωd((n log n)1/(d−1)) against depth-d circuits for inverse trace over binary fields, the Goldreich–Tal trilinear function and OpenAI's polynomial evaluator with its original parameters, improving Chukhin's bound; also a correlation bound for inverse trace.	arXiv preprint.

Notes

• The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.