Lean statement

Depth-three circuit lower bound beyond every square-root constant

Lean is a language for mathematical statements and proofs that a computer can verify. This page shows one statement file from OpenAI’s release, possible paper matches and independent reports. The code-like names below identify the definitions or theorems selected by the proof-verification settings.

Theorem selected for verification: OAI.DepthThreeLowerBound.exists_polynomial_time_language_depth_three_lower_bound

Lean statement file: DepthThree.leanShow on the mapFamily 112. OpenAI lists this as a main result in its Lean catalogue.

See the candidate theorem Who ran the proof-verification program Report a comparison with the paper (GitHub issue)

The Lean statement

The lines of the Lean statement that state the theorem, then the definitions in the file that it uses.

theorem exists_polynomial_time_language_depth_three_lower_bound :    ∃ (L : List Bool → Bool) (M : FiniteMultiTapeMachine) (C a : ℕ),      0 < C ∧ 0 < a ∧      (∀ w : List Bool, MultiTapeHaltsIn M w (L w) (C * (w.length + 1) ^ a)) ∧      ∀ A : ℝ, 0 < A → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →        ∀ D : Circuit3 (Fin n), D.Computes (fun x => L (List.ofFn x)) →          (2 : ℝ) ^ (A * Real.sqrt (n : ℝ)) < (D.gateCount : ℝ) := by  sorry

A Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.

Definitions needed to read it

Local definitions the statement names, followed through the definitions they name in turn. The match is by name in the source text, so a name reached only through notation can be missed; the full file is below.

abbreviation OAI.DepthThreeLowerBound.Cube line 9
```
abbrev Cube (V : Type uV) := V → Bool
```
abbreviation OAI.DepthThreeLowerBound.Literal line 10
```
abbrev Literal (V : Type uV) := V × Bool
```

definition OAI.DepthThreeLowerBound.Literal.eval line 16

def eval (l : Literal V) (x : Cube V) : Bool := decide (x l.1 = l.2)

abbreviation OAI.DepthThreeLowerBound.GateInput line 20

abbrev GateInput (V : Type uV) := Sum (Literal V) Bool

abbreviation OAI.DepthThreeLowerBound.RawClause line 21

abbrev RawClause (V : Type uV) := List (GateInput V)

structure OAI.DepthThreeLowerBound.Circuit3 line 39

structure Circuit3 (V : Type uV) where  bottomCount : ℕ  middleCount : ℕ  bottom : Fin bottomCount → RawClause V  middle : Fin middleCount → Finset (Fin bottomCount)  top : Finset (Fin middleCount)

definition OAI.DepthThreeLowerBound.Circuit3.gateCount line 48

def gateCount (C : Circuit3 V) : ℕ := C.bottomCount + C.middleCount + 1

definition OAI.DepthThreeLowerBound.Circuit3.Computes line 59

def Computes (C : Circuit3 V) (f : Cube V → Bool) : Prop := ∀ x, C.eval x = f x

definition OAI.DepthThreeLowerBound.runSteps line 63

def runSteps {S : Type uS} (step : S → Option S) (n : ℕ) (c : Option S) : Option S :=  (fun oc => oc.bind step)^[n] c

inductive type OAI.DepthThreeLowerBound.HeadMove line 66
```
inductive HeadMove  | left  | stay  | right
```

definition OAI.DepthThreeLowerBound.HeadMove.apply line 71

def HeadMove.apply {Γ : Type uGamma} [Inhabited Γ] : HeadMove → Turing.Tape Γ → Turing.Tape Γ  | .left, t => t.move Turing.Dir.left  | .stay, t => t  | .right, t => t.move Turing.Dir.right

structure OAI.DepthThreeLowerBound.MultiTapeCfg line 76

structure MultiTapeCfg (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) [Inhabited Γ] where  q : Q  tapes : K → Turing.Tape Γ

abbreviation OAI.DepthThreeLowerBound.MultiTapeCode line 80

abbrev MultiTapeCode (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) :=  Q → (K → Γ) → Option (Q × (K → Γ) × (K → HeadMove))

definition OAI.DepthThreeLowerBound.multiTapeUpdate line 83

def multiTapeUpdate {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (c : MultiTapeCfg K Γ Q)    (q : Q) (writes : K → Γ) (moves : K → HeadMove) : MultiTapeCfg K Γ Q :=  ⟨q, fun k => (moves k).apply ((c.tapes k).write (writes k))⟩

definition OAI.DepthThreeLowerBound.multiTapeStep line 87

def multiTapeStep {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (code : MultiTapeCode K Γ Q)    (c : MultiTapeCfg K Γ Q) : Option (MultiTapeCfg K Γ Q) :=  (code c.q (fun k => (c.tapes k).head)).map fun out =>    multiTapeUpdate c out.1 out.2.1 out.2.2

structure OAI.DepthThreeLowerBound.FiniteMultiTapeMachine line 92

structure FiniteMultiTapeMachine where

Show the remaining 15 lines

  K : Type  [tapeFinite : Fintype K]  [tapeDecidableEq : DecidableEq K]  inputTape : K  Γ : Type  [alphabetInhabited : Inhabited Γ]  [alphabetFinite : Fintype Γ]  Q : Type  [stateFinite : Fintype Q]  initialState : Q  inputSymbol : Bool → Γ  input_injective : Function.Injective inputSymbol  input_ne_blank : ∀ b, inputSymbol b ≠ default  code : MultiTapeCode K Γ Q  accept : Q → Bool

abbreviation OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.Cfg line 115
```
abbrev Cfg (M : FiniteMultiTapeMachine) := MultiTapeCfg M.K M.Γ M.Q
```

abbreviation OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.step line 117

abbrev step (M : FiniteMultiTapeMachine) : M.Cfg → Option M.Cfg :=  multiTapeStep M.code

definition OAI.DepthThreeLowerBound.FiniteMultiTapeMachine.init line 120

def init (M : FiniteMultiTapeMachine) (input : List Bool) : M.Cfg :=  ⟨M.initialState, fun k =>    if k = M.inputTape then Turing.Tape.mk₁ (input.map M.inputSymbol)    else Turing.Tape.mk₁ []⟩

definition OAI.DepthThreeLowerBound.MultiTapeHaltsIn line 127

def MultiTapeHaltsIn (M : FiniteMultiTapeMachine) (input : List Bool)    (output : Bool) (time : ℕ) : Prop :=  ∃ k ≤ time, ∃ c : M.Cfg,    runSteps M.step k (some (M.init input)) = some c ∧    M.step c = none ∧ M.accept c.q = output

Possible paper match, with no recorded review

Atlas selected this possible match by comparing words in the Lean statement with every statement in the family. No review of whether the statements mean the same thing is recorded.

Words of the Lean statement, its names split into words, that also appear in the theorem: bottom, circuits, function, runs, time, real, language, sqrt and six more. Found in the paper’s title, which its main theorem states: depth and three. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: fan.

Theorem 1.1 of Beyond the Square-Root Exponent for Depth-Three Boolean Circuits

Theorem

There is a language L\subseteq\bits^*, a deterministic Turing machine deciding L, and fixed positive integers C,a such that the machine runs in time at most C(n+1)^a on every input of length n. If f_n is the membership function of L on \bits^n, then

\lim_{n\to\infty}\frac{\log_2 S_3(f_n)}{\sqrt n}=\infty.

Equivalently, for every real A>0, there is an integer N_A such that

S_3(f_n)>2^{A\sqrt n}\qquad\text{for every }n\ge N_A.

No uniformity or bottom fan-in restriction is imposed on the circuits.

Section 1, Introduction Read it in the paper TeX source, line 21

Show the TeX

There is a language \(L\subseteq\bits^*\), a deterministic Turing machine
deciding \(L\), and fixed positive integers \(C,a\) such that the machine
runs in time at most \(C(n+1)^a\) on every input of length \(n\).
If \(f_n\) is the membership function of \(L\) on \(\bits^n\), then
\[
 \lim_{n\to\infty}\frac{\log_2 S_3(f_n)}{\sqrt n}=\infty.
\]
Equivalently, for every real \(A>0\), there is an integer \(N_A\)
such that
\[
 S_3(f_n)>2^{A\sqrt n}\qquad\text{for every }n\ge N_A.
\]
No uniformity or bottom fan-in restriction is imposed on the circuits.

Other possible paper matches, closest wording first

Proposition 5.2 of Beyond the Square-Root Exponent for Depth-Three Boolean Circuits. Words of the Lean statement, its names split into words, that also appear in the theorem: time, language, turing, machine, decided, input and two more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: one.
Proposition 5.3 of Beyond the Square-Root Exponent for Depth-Three Boolean Circuits. Words of the Lean statement, its names split into words, that also appear in the theorem: bound, real, sqrt, lengths and integer. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: resulting.

How Atlas selects possible matches: it compares words in the Lean statement with every statement in the family. It also splits Lean names into words. The release’s label and note receive less weight; a main theorem wins a close match. If the Lean wording yields no clear match, Atlas uses the catalogue description. This selects passages to compare; it does not establish that they mean the same thing.

Reported Comparator runs

two independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet. Each group reports its own Comparator run for this statement file. Atlas has not repeated the runs.

For a configured theorem, Comparator tests whether OpenAI’s proof proves the exact Lean statement. Some files instead configure definitions for comparison by name and type. Acceptance does not establish that the statement means the same thing as the paper’s theorem.

Carlos Toledo’s cert-machine

How they ran it, in their words

Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners (.github/workflows/openai-math-kernel.yml), one j…

Accepted Their term: “CERTIFIED”.
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Reported 10 October 2026, at the release version shown here. Original verification report

MathVet

How they ran it, in their words

An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.

Accepted Their term: “comparator-sandboxed-pass”.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Reported 8 October 2026, at the release version shown here. Original verification report

What an accepted Comparator run would establish

If Comparator is run under this configuration and accepts, the solution proves the configured theorem using only the allowed axioms, and the Lean kernel accepts every step.

This configuration lists no definition holes, so every definition the statement uses is compared as it is written in this file.

Allowed axioms: propext, Quot.sound, Classical.choice

Acceptance leaves open whether the Lean statement means the same thing as the paper’s theorem, whether the paper’s other claims are correct, and whether the result is new. Those questions require comparing the definitions and statements, reviewing the paper’s arguments, and reading the earlier literature.

Do family 112’s Lean statements express the advertised result?

These assessments compare all the family’s Lean statements with the whole result OpenAI describes in its catalogue. They do not assess this statement alone. Each group uses its own published rules.

MathVet and cert-machine agree on how much of the advertised result the Lean statements express.

MathVet
Finds the whole advertised result stated or implied Their term: “full”.
The challenge statements imply the headline claim after unpacking definitions or one routine step. Their record
Their note: None; as the docs say, no fixed exponent n^{1/2+eps} and no unrestricted-depth bound is asserted.
Definitions the group asks readers to compare with the paper: Polynomial time is measured on a hand-rolled FiniteMultiTapeMachine (finite tapes/alphabet/states, Mathlib Turing.Tape, MultiTapeHaltsIn = halts within C*(|w|+1)^a steps), not Mathlib's TM2ComputableInPolyTime; the circuit class Circuit3 is a custom inductive encoding with free negations/constants (standard)
Carlos Toledo’s cert-machine
Finds the whole advertised result stated or implied Their term: “MATCHES”.
The challenge statements state the headline as OpenAI wrote it. Their record

Read the complete assessments on the family page.

OpenAI’s own note on what this Lean statement covers

“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.”
Quoted from OpenAI’s Lean note for this family

An AI agent drafted an interpretation of that note, classifying this statement as “states a paper’s theorem as the paper does”. No human review of the draft is recorded.

Supporting material

The complete Lean statement file

144 lines, copied from release version fd4aeeb. A name defined in this file links to its line; pointing at the name shows its definition.

Declared in this fileOpenAI’s library at fd4aeebOther linked names open the current documentation for Mathlib, Lean’s mathematical library.

Links in the file: 41 to its own declarations, 64 to Mathlib’s documentation. 25 declared names also link to the same declaration in OpenAI’s library. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

Definitions and lemmas named by the statement

If Comparator accepts a proof, it proves exists_polynomial_time_language_depth_three_lower_bound exactly as written here. To compare that statement with the paper, also read the definitions and lemmas listed below. Atlas found them by following names in the source text and lists each after the names it uses. For x.foo, Atlas includes every foo defined here for a type, even when the statement may use only one of them.

It reaches 23 of the file’s 24 other declarations; with the theorem itself they span 80 lines. 5 of them are named in the statement itself.

Names in the namespace OAI.DepthThreeLowerBound are listed without it.

abbrev Cubeline 9library
abbrev Literalline 10library
def Literal.evalline 16library
abbrev GateInputline 20library
abbrev RawClauseline 21library
def GateInput.evalline 25library
def RawClause.evalline 33library
structure Circuit3line 39in the statementlibrary
def Circuit3.gateCountline 48in the statementlibrary
def Circuit3.middleEvalline 50library
def Circuit3.evalline 55library
def Circuit3.Computesline 59in the statementlibrary
def runStepsline 63library
inductive HeadMoveline 66library
structure MultiTapeCfgline 76library
abbrev MultiTapeCodeline 80library
def multiTapeUpdateline 83library
def multiTapeStepline 87library
structure FiniteMultiTapeMachineline 92in the statementlibrary
abbrev FiniteMultiTapeMachine.Cfgline 115library
abbrev FiniteMultiTapeMachine.stepline 117library
def FiniteMultiTapeMachine.initline 120library
def MultiTapeHaltsInline 127in the statementlibrary
theorem exists_polynomial_time_language_depth_three_lower_boundline 133selected theoremlibrary

Other Lean rules that may affect the statement 1

Lean can use instances, notation and attributes without naming them in the statement. These are rules for interpreting or finding mathematical objects. Atlas’s scan of names cannot follow all such uses; read the listed source as well.

attribute [instance] FiniteMultiTapeMachine.tapeFinite line 109

1 declaration the statement does not reach by name

These definitions and lemmas were not found by following names in the statement. Lean may still use them through rules such as instances or macros.

def apply line 71

import Mathlibnamespace OAInamespace DepthThreeLowerBounduniverse uV uS uK uGamma uQabbrev Cube (V : Type uV) := V → Boolabbrev Literal (V : Type uV) := V × Boolvariable {V : Type uV}namespace Literaldef eval (l : Literal V) (x : Cube V) : Bool := decide (x l.1 = l.2)end Literalabbrev GateInput (V : Type uV) := Sum (Literal V) Boolabbrev RawClause (V : Type uV) := List (GateInput V)namespace GateInputdef eval : GateInput V → Cube V → Bool  | .inl l, x => l.eval x  | .inr b, _ => bend GateInputnamespace RawClausenoncomputable def eval (C : RawClause V) (x : Cube V) : Bool := by  classical  exact decide (∃ l ∈ C, l.eval x = true)end RawClausestructure Circuit3 (V : Type uV) where  bottomCount : ℕ  middleCount : ℕ  bottom : Fin bottomCount → RawClause V  middle : Fin middleCount → Finset (Fin bottomCount)  top : Finset (Fin middleCount)namespace Circuit3def gateCount (C : Circuit3 V) : ℕ := C.bottomCount + C.middleCount + 1noncomputable def middleEval (C : Circuit3 V) (j : Fin C.middleCount)    (x : Cube V) : Bool := by  classical  exact decide (∀ i ∈ C.middle j, (C.bottom i).eval x = true)noncomputable def eval (C : Circuit3 V) (x : Cube V) : Bool := by  classical  exact decide (∃ j ∈ C.top, C.middleEval j x = true)def Computes (C : Circuit3 V) (f : Cube V → Bool) : Prop := ∀ x, C.eval x = f xend Circuit3def runSteps {S : Type uS} (step : S → Option S) (n : ℕ) (c : Option S) : Option S :=  (fun oc => oc.bind step)^[n] cinductive HeadMove  | left  | stay  | rightdef HeadMove.apply {Γ : Type uGamma} [Inhabited Γ] : HeadMove → Turing.Tape Γ → Turing.Tape Γ  | .left, t => t.move Turing.Dir.left  | .stay, t => t  | .right, t => t.move Turing.Dir.rightstructure MultiTapeCfg (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) [Inhabited Γ] where  q : Q  tapes : K → Turing.Tape Γabbrev MultiTapeCode (K : Type uK) (Γ : Type uGamma) (Q : Type uQ) :=  Q → (K → Γ) → Option (Q × (K → Γ) × (K → HeadMove))def multiTapeUpdate {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (c : MultiTapeCfg K Γ Q)    (q : Q) (writes : K → Γ) (moves : K → HeadMove) : MultiTapeCfg K Γ Q :=  ⟨q, fun k => (moves k).apply ((c.tapes k).write (writes k))⟩def multiTapeStep {K : Type uK} {Γ : Type uGamma} {Q : Type uQ} [Inhabited Γ] (code : MultiTapeCode K Γ Q)    (c : MultiTapeCfg K Γ Q) : Option (MultiTapeCfg K Γ Q) :=  (code c.q (fun k => (c.tapes k).head)).map fun out =>    multiTapeUpdate c out.1 out.2.1 out.2.2structure FiniteMultiTapeMachine where  K : Type  [tapeFinite : Fintype K]  [tapeDecidableEq : DecidableEq K]  inputTape : K  Γ : Type  [alphabetInhabited : Inhabited Γ]  [alphabetFinite : Fintype Γ]  Q : Type  [stateFinite : Fintype Q]  initialState : Q  inputSymbol : Bool → Γ  input_injective : Function.Injective inputSymbol  input_ne_blank : ∀ b, inputSymbol b ≠ default  code : MultiTapeCode K Γ Q  accept : Q → Boolattribute [instance] FiniteMultiTapeMachine.tapeFinite  FiniteMultiTapeMachine.tapeDecidableEq FiniteMultiTapeMachine.alphabetInhabited  FiniteMultiTapeMachine.alphabetFinite FiniteMultiTapeMachine.stateFinitenamespace FiniteMultiTapeMachineabbrev Cfg (M : FiniteMultiTapeMachine) := MultiTapeCfg M.K M.Γ M.Qabbrev step (M : FiniteMultiTapeMachine) : M.Cfg → Option M.Cfg :=  multiTapeStep M.codedef init (M : FiniteMultiTapeMachine) (input : List Bool) : M.Cfg :=  ⟨M.initialState, fun k =>    if k = M.inputTape then Turing.Tape.mk₁ (input.map M.inputSymbol)    else Turing.Tape.mk₁ []⟩end FiniteMultiTapeMachinedef MultiTapeHaltsIn (M : FiniteMultiTapeMachine) (input : List Bool)    (output : Bool) (time : ℕ) : Prop :=  ∃ k ≤ time, ∃ c : M.Cfg,    runSteps M.step k (some (M.init input)) = some c ∧    M.step c = none ∧ M.accept c.q = outputtheorem exists_polynomial_time_language_depth_three_lower_bound :    ∃ (L : List Bool → Bool) (M : FiniteMultiTapeMachine) (C a : ℕ),      0 < C ∧ 0 < a ∧      (∀ w : List Bool, MultiTapeHaltsIn M w (L w) (C * (w.length + 1) ^ a)) ∧      ∀ A : ℝ, 0 < A → ∃ N : ℕ, ∀ n : ℕ, N ≤ n →        ∀ D : Circuit3 (Fin n), D.Computes (fun x => L (List.ofFn x)) →          (2 : ℝ) ^ (A * Real.sqrt (n : ℝ)) < (D.gateCount : ℝ) := by  sorryend DepthThreeLowerBoundend OAI

Every extracted statement of the accompanying papers

The statements the atlas extracted automatically from each accompanying paper’s TeX source, with links to the full sources.

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