Explicit depth-three circuit lower bounds beyond the square-root exponent

Theorem 1.1: there is a language $L$ decidable by a deterministic Turing machine in time $C(n+1)^a$ whose $n$ -bit membership functions satisfy $\log_2 S_3(f_n)/\sqrt n\to\infty$ , counting all gates of OR-AND-OR circuits with no fan-in restriction. The language and machine are fixed before the constant $A$ . It does not give a fixed exponent $n^{1/2+\varepsilon}$ (Hastad-Jukna-Pudlak's problem stays open), says nothing about AND-OR-AND circuits beyond what duality gives for the complement, and nothing about depth above three or Valiant's $2^{\omega(n/\log\log n)}$ threshold.

Exact FrontierDelta

Prior state unknown→proved

Scope and record

Occurred: Sep 23, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-checked. Publication: announcement. AI contribution: ai-discovered. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Explicit depth-three circuit lower bounds beyond the square-root exponent · Depth-three lower bounds beyond 2^O(sqrt n)

Confidence: Not scored

Registry verification: lean checked · announcement · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

Unreleased internal OpenAI model
model · ai model contributor · OpenAI

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Explicit depth-three circuit lower bounds beyond the square-root exponent

specialist registry · passed

No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the question as the manuscript and its cited sources pose it. The proof was not refereed. lean/formalization.yaml lists a main result for this manuscript (comparator DepthThree, declaration OAI.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound). The statement ComparatorChallenges/DepthThree.lean was read: there are a language $L$ , a finite multitape Turing machine deciding it within $C(n+1)^a$ steps on every input, and for every real $A>0$ an $N$ such that every OR-AND-OR circuit (literal and constant inputs, arbitrary fan-in and sharing, all gates counted) computing $L$ on $n\ge N$ bits has more than $2^{A\sqrt n}$ gates. This states the headline claim. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.