Time-capped and unknown-time one-tape simulation in two-fifths-power space (Lean)

The Lean statement

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

theorem capped [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :    ∃ (N : TM X Unit M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧      ∀ (x : List X) (T : ℕ), 2 ≤ T → M.Access A p q x T →        ∃ b : ℕ, N.Within (binaryIn x (fun _ => T)) (M.outcome x T) b ∧          (b:ℝ) ≤ c*(T:ℝ)^exponent*(Log T)^e := by  sorry⋮theorem unknown [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :    ∃ (N : TM X Empty M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧      ∀ (x : List X), (∀ T, 2 ≤ T → M.Access A p q x T) →        ∀ (t : ℕ), (M.outcome x t).2 = true →          ∃ b, N.Within (files x) (M.outcome x t) b ∧            (b:ℝ) ≤ c*((t:ℝ)+2)^exponent*(Log t)^e := 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.

inductive type OAI.Fifths.Dir line 11

inductive Dir  | L | N | R  deriving DecidableEq

definition OAI.Fifths.Dir.delta line 18

@[simp] def delta : Dir → ℤ  | L => -1  | N => 0  | R => 1

inductive type OAI.Fifths.Mark line 24

inductive Mark (A : Type)  | left  | sym (a : A)  | right  deriving DecidableEq, Fintype

definition OAI.Fifths.Mark.see line 32

def see (w : List A) : ℕ → Mark A  | 0 => left  | p+1 =>    match w[p]? with    | some a => sym a    | none => right

definition OAI.Fifths.Mark.walk line 39

def walk (w : List A) (p : ℕ) : Dir → ℕ  | .N => p  | .L => p - 1  | .R => if w.length < p then p else p + 1

inductive type OAI.Fifths.Runs line 45

inductive Runs {σ Y : Type} (f : σ → Y ⊕ σ) (P : σ → Prop) :    σ → σ → Y → Prop  | stop {s y} (ok : P s) (eqn : f s = Sum.inl y) : Runs f P s s y  | step {s s' t y} (ok : P s) (eqn : f s = Sum.inr s')      (tail : Runs f P s' t y) : Runs f P s t y

structure OAI.Fifths.Inputs line 51

structure Inputs (X J : Type) where  publicWord : List X  arg : J → List Bool

structure OAI.Fifths.Readers line 55

structure Readers (J : Type) where  px : ℕ := 0  parg : J → ℕ := fun _ => 0

structure OAI.Fifths.Reads line 59

structure Reads (X J : Type) where  sx : Mark X  sarg : J → Mark Bool

structure OAI.Fifths.Advances line 63

structure Advances (J : Type) where  dx : Dir := .N  darg : J → Dir := fun _ => .N

definition OAI.Fifths.Readers.home line 69
```
def home : Readers J := {}
```

structure OAI.Fifths.Tape line 76

structure Tape (A : Type) where  pos : ℤ  sym : ℤ → A

structure OAI.Fifths.WriteMove line 80

structure WriteMove (A : Type) where  sym : A  dir : Dir

definition OAI.Fifths.Tape.init line 86

def init (a : A) : Tape A := ⟨0, fun _ => a⟩

definition OAI.Fifths.Tape.perform line 88

def perform (w : Tape A) (m : WriteMove A) : Tape A :=  ⟨w.pos + m.dir.delta, Function.update w.sym w.pos m.sym⟩

structure OAI.Fifths.TAction line 92

structure TAction (Q J K : Type) (W : K → Type) where  next : Q  advance : Advances J  moves : ∀ k : K, WriteMove (W k)

structure OAI.Fifths.TM line 97

structure TM (X J Y : Type) where  Q : Type  [finiteQ : Finite Q]  K : Type  [tapes : Fintype K]  W : K → Type  [symbols : ∀ k, Fintype (W k)]  blank : ∀ k, W k  start : Q  table : Q → Reads X J → ((k : K) → W k) → Y ⊕ TAction Q J K W

structure OAI.Fifths.TM.Cfg line 113

structure Cfg where  state : M.Q  ro : Readers J  work : ∀ k, Tape (M.W k)

definition OAI.Fifths.TM.initial line 118

def initial : M.Cfg :=  ⟨M.start, .home, fun k => .init (M.blank k)⟩

definition OAI.Fifths.TM.step line 121

def step (i : Inputs X J) (s : M.Cfg) : Y ⊕ M.Cfg :=  match M.table s.state (s.ro.see i) (fun k => (s.work k).see) with  | Sum.inl y => .inl y  | Sum.inr a =>    .inr ⟨a.next, s.ro.walk i a.advance, fun k => (s.work k).perform (a.moves k)⟩

structure OAI.Fifths.TM.Window line 127

structure Window where  l : M.K → ℕ  h : M.K → ℕ

definition OAI.Fifths.TM.width line 131

def width (k : M.K) : ℕ := max 1 (Fintype.card (M.W k) - 1).size

definition OAI.Fifths.TM.Window.ok line 135

def ok (w : M.Window) (s : M.Cfg) : Prop :=  ∀ k, -(w.l k : ℤ) ≤ (s.work k).pos ∧ (s.work k).pos ≤ (w.h k : ℤ)

definition OAI.Fifths.TM.Window.bits line 138

def bits (w : M.Window) : ℕ :=  ∑ k, (w.l k + w.h k + 1) * M.width k

21 more definitions are reached the same way; the full file lists them.

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: 2/5, steps, functions, cap, finite, public, access, tape and eleven more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: simulation, independent, control, deterministic, machine, writable, one and space.

Theorem 1 of Simulating One-Tape Time in Two-Fifths-Power Space

Theorem

Fix a deterministic machine with one writable tape and head, a fixed number of read-only input heads, unit movement and fixed origins for all heads, cap-independent symbol functions, and a fixed accessor as above. For every public input x and supplied binary cap T\ge2 for which the access condition holds, its finite-control and halting outcome by time T can be computed deterministically in \softO(T^{2/5}) work-space bits, excluding storage for the read-only input. Simulation time is unrestricted, and the final writable tape need not be materialized. If the access condition holds for (x,T) at every T\ge2, and the machine halts on x after t steps without a supplied running time, its outcome can be computed in \softO((t+2)^{2/5}) work-space bits.

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

Show the TeX

Fix a deterministic machine with one writable tape and head, a fixed
number of read-only input heads, unit movement and fixed origins for
all heads, cap-independent symbol functions, and a fixed accessor as above.
For every public input \(x\) and supplied binary cap \(T\ge2\) for which
the access condition
holds, its finite-control and halting outcome by time \(T\) can be
computed deterministically in \(\softO(T^{2/5})\) work-space bits,
excluding storage for the read-only input. Simulation time is
unrestricted, and the final writable tape need not be materialized.
If the access condition holds for \((x,T)\) at every \(T\ge2\), and
the machine halts on \(x\) after \(t\) steps without a supplied running
time, its outcome can be computed in
\(\softO((t+2)^{2/5})\) work-space bits.

Other possible paper matches, closest wording first

Proposition 11 of Simulating One-Tape Time in Two-Fifths-Power Space. Words of the Lean statement, its names split into words, that also appear in the theorem: tapes, functions, cap, finite, public, access and eleven more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: simulation, independent, control, deterministic, machine, writable and one more.
Corollary 13 of Simulating One-Tape Time in Two-Fifths-Power Space. Words of the Lean statement, its names split into words, that also appear in the theorem: ro, halting, input and time. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: bounded, many, one and space.
Corollary 12 of Simulating One-Tape Time in Two-Fifths-Power Space. Words of the Lean statement, its names split into words, that also appear in the theorem: ro, tape and time. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: writable, one and space.

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

three independent groups report that Comparator accepted runs for this Lean statement file: Carlos Toledo’s cert-machine; MathVet; Neal McBurnett’s openai-math-lean-tooling. 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 10 October 2026, at the release version shown here. Original verification report

Neal McBurnett’s openai-math-lean-tooling

How they ran it, in their words

Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory; the run was still in progress at this snapshot (192 accepted, 224 pending).

Accepted Their term: “accepted”.
Re-run through Comparator with Lean’s kernel: accepted (the check took 91 s; peak memory 6.2 GiB).
Reported 11 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, Classical.choice, Quot.sound

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 137’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: Lean capped and unknown are the two clauses of the paper's single main theorem (introduction.tex:64-79) with Single = the fixed one-writable-tape machine, Access = the polylog-space accessor condition, outcome = (finite-control state, halted flag) with absorbing halting states, Within = work-space bits with no time bound, and c*T^(2/5)*(log2(T+2))^e = O~(T^{2/5}); no step beyond unfolding these definitions is needed. The summary's remark 'improving the square-root exponent' is a comparison with the classical bound, not a separate formal claim.
Definitions the group asks readers to compare with the paper: Single.sensor: initial writable-tape contents (tag none) and the symbols read by each of the heads read-only heads (tag some i) are an arbitrary function List X -> Option (Fin heads) -> Z -> A, constrained only through the Access hypothesis; input symbols share the tape alphabet A. This is the paper's 'uniform interface' (introduction.tex:33-38), not a restriction. The tape contents sensor x none do not depend on T by construction. ; Single.Access: the polylog-space accessor hypothesis is part of the statement (the theorem is conditional on it, per pair (x,T), as in the paper): a fixed uniform TM A, given x, the cap T, the tag, and the sign and magnitude of l in binary, outputs sensor x h l within p*(log2(T+2))^q work bits for every tag and every |l| <= T. In unknown it is required for every T >= 2. ; TM / TM.Within / Window.bits: simulator and accessor model is a multi-tape machine (finite Q, finitely many work tapes with finite alphabets) with endmarked read-only heads on the public word and on each binary argument tape; space = sum over work tapes of (window span including the origin) * bit-width of the alphabet; input and cap tapes are not charged; NO time bound (matches 'simulation time is unrestricted'); standard counted-cell convention. ; Single.move / Single.outcome: halted states are absorbing (state, tape symbol and head positions unchanged), and outcome x n = (state, halted flag) after exactly n steps, so it equals the 'finite-control and halting outcome by time n'. ; [Fintype X]: the public alphabet is finite. ; Cost.Log / Cost.exponent: Log T = Real.log (T+2) / Real.log 2 (binary log of T+2); exponent = 2/5 used as a real power; the log exponent e is a natural number and c a positive real, both existentially quantified before x and T (they may depend on M, A, p, q only), matching O~ with 'a fixed constant C'. ; Mark.see / Mark.walk: read-only inputs are endmarked (0 = left marker, 1..len = symbols, len+1 = right marker) and heads are confined to [0, len+1]; 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 formalization gives two-fifths-power space simulation of a fixed deterministic machine with one writable tape and finitely many read-only input heads. Heads move at most one cell per step, initial contents are independent of the time bound, and contents and input symbols must be accessible in polylogarithmic space. Given a binary time cap $T\ge2$, the simulator returns the source's finite-control outcome and halting flag using $O(T^{2/5}(\log(T+2))^C)$ space.”
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

275 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: 78 to its own declarations, 63 to Mathlib’s documentation. 51 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.

import Mathlibnamespace OAI/-! Finite-machine statements of the capped and unknown-time one-writable-tapesimulation theorem. Work space counts the bits in every visited writable cell;public endmarked input tapes are read-only. -/namespace Fifthsinductive Dir  | L | N | R  deriving DecidableEqinstance : Fintype Dir := ⟨{.L, .N, .R}, by intro d; cases d <;> simp⟩namespace Dir@[simp] def delta : Dir → ℤ  | L => -1  | N => 0  | R => 1end Dirinductive Mark (A : Type)  | left  | sym (a : A)  | right  deriving DecidableEq, Fintypenamespace Markvariable {A : Type}def see (w : List A) : ℕ → Mark A  | 0 => left  | p+1 =>    match w[p]? with    | some a => sym a    | none => rightdef walk (w : List A) (p : ℕ) : Dir → ℕ  | .N => p  | .L => p - 1  | .R => if w.length < p then p else p + 1end Markinductive Runs {σ Y : Type} (f : σ → Y ⊕ σ) (P : σ → Prop) :    σ → σ → Y → Prop  | stop {s y} (ok : P s) (eqn : f s = Sum.inl y) : Runs f P s s y  | step {s s' t y} (ok : P s) (eqn : f s = Sum.inr s')      (tail : Runs f P s' t y) : Runs f P s t ystructure Inputs (X J : Type) where  publicWord : List X  arg : J → List Boolstructure Readers (J : Type) where  px : ℕ := 0  parg : J → ℕ := fun _ => 0structure Reads (X J : Type) where  sx : Mark X  sarg : J → Mark Boolstructure Advances (J : Type) where  dx : Dir := .N  darg : J → Dir := fun _ => .Nnamespace Readersvariable {X J : Type}def home : Readers J := {}def see (r : Readers J) (i : Inputs X J) : Reads X J :=  ⟨Mark.see i.publicWord r.px, fun j => Mark.see (i.arg j) (r.parg j)⟩def walk (r : Readers J) (i : Inputs X J) (a : Advances J) : Readers J :=  ⟨Mark.walk i.publicWord r.px a.dx, fun j => Mark.walk (i.arg j) (r.parg j) (a.darg j)⟩end Readersstructure Tape (A : Type) where  pos : ℤ  sym : ℤ → Astructure WriteMove (A : Type) where  sym : A  dir : Dirnamespace Tapevariable {A : Type}def init (a : A) : Tape A := ⟨0, fun _ => a⟩def see (w : Tape A) : A := w.sym w.posdef perform (w : Tape A) (m : WriteMove A) : Tape A :=  ⟨w.pos + m.dir.delta, Function.update w.sym w.pos m.sym⟩end Tapestructure TAction (Q J K : Type) (W : K → Type) where  next : Q  advance : Advances J  moves : ∀ k : K, WriteMove (W k)structure TM (X J Y : Type) where  Q : Type  [finiteQ : Finite Q]  K : Type  [tapes : Fintype K]  W : K → Type  [symbols : ∀ k, Fintype (W k)]  blank : ∀ k, W k  start : Q  table : Q → Reads X J → ((k : K) → W k) → Y ⊕ TAction Q J K Wattribute [instance] TM.finiteQ TM.tapes TM.symbolsnamespace TMvariable {X J Y : Type} (M : TM X J Y)structure Cfg where  state : M.Q  ro : Readers J  work : ∀ k, Tape (M.W k)def initial : M.Cfg :=  ⟨M.start, .home, fun k => .init (M.blank k)⟩def step (i : Inputs X J) (s : M.Cfg) : Y ⊕ M.Cfg :=  match M.table s.state (s.ro.see i) (fun k => (s.work k).see) with  | Sum.inl y => .inl y  | Sum.inr a =>    .inr ⟨a.next, s.ro.walk i a.advance, fun k => (s.work k).perform (a.moves k)⟩structure Window where  l : M.K → ℕ  h : M.K → ℕdef width (k : M.K) : ℕ := max 1 (Fintype.card (M.W k) - 1).sizenamespace Windowvariable {M}def ok (w : M.Window) (s : M.Cfg) : Prop :=  ∀ k, -(w.l k : ℤ) ≤ (s.work k).pos ∧ (s.work k).pos ≤ (w.h k : ℤ)open BigOperatorsdef bits (w : M.Window) : ℕ :=  ∑ k, (w.l k + w.h k + 1) * M.width kend Windowdef Within (i : Inputs X J) (y : Y) (S : ℕ) : Prop :=  ∃ w : M.Window, w.bits ≤ S ∧ ∃ t, Runs (M.step i) w.ok M.initial t yend TMend Fifthsnamespace Fifthsstructure SingleAct (Q A : Type) (r : ℕ) where  out : Q  write : WriteMove A  others : Fin r → Dirstructure Single (X : Type) where  Q : Type  [states : Fintype Q]  A : Type  [symbols : Fintype A]  beginState : Q  halted : Q → Bool  heads : ℕ  program : Q → A → (Fin heads → A) → SingleAct Q A heads  sensor : List X → Option (Fin heads) → ℤ → Aattribute [instance] Single.states Single.symbolsnamespace Singlevariable {X : Type} (M : Single X)instance : Nonempty M.A := ⟨M.sensor [] none 0⟩instance : Nonempty M.Q := ⟨M.beginState⟩abbrev Tag := Option (Fin M.heads)structure At where  state : M.Q  tape : Tape M.A  ro : Fin M.heads → ℤdef move (q : M.Q) (s : M.A) (r : Fin M.heads → M.A) :    SingleAct M.Q M.A M.heads :=  if M.halted q then    ⟨q,⟨s,.N⟩,fun _ => .N⟩  else M.program q s rdef initial (x : List X) : M.At :=  ⟨M.beginState,⟨0,M.sensor x none⟩, fun _ => 0⟩def next (x : List X) (s : M.At) : M.At :=  let t := M.move s.state s.tape.see (fun i => M.sensor x (some i) (s.ro i))  ⟨t.out,s.tape.perform t.write,fun i => s.ro i + (t.others i).delta⟩def atTime (M : Single X) (x : List X) : ℕ → M.At :=  Nat.rec (M.initial x) (fun _ s => M.next x s)abbrev Outcome := M.Q × Booldef finish (q : M.Q) : M.Outcome :=  (q, M.halted q)def outcome (x : List X) (n : ℕ) : M.Outcome :=  M.finish (M.atTime x n).statedef Inside (t : ℕ) (q : ℤ) : Prop := -(t:ℤ) ≤ q ∧ q ≤ (t:ℤ)end Singleend Fifthsnamespace Fifthsnamespace Entrynoncomputable def code {A : Type} [Fintype A] (a : A) : ℕ :=  (Fintype.equivFin A a).valend Entrydef binaryIn {X J : Type} (pub : List X) (f : J → ℕ) : Inputs X J :=  ⟨pub, fun j => (f j).bits⟩def files {X : Type} (x : List X) : Inputs X Empty :=  ⟨x, Empty.elim⟩namespace Singleopen Entryvariable {X : Type} (M : Single X)inductive Arg  | cap | tag | minus | magnitude  deriving DecidableEqinstance : Fintype Arg :=  ⟨{.cap, .tag, .minus, .magnitude}, by intro a; cases a <;> simp⟩abbrev Sym := TM X Arg M.Anoncomputable def arg (T : ℕ) (h : M.Tag) (p : ℤ) : Arg → ℕ  | .cap => T  | .tag => code h  | .minus => (decide (p < 0)).toNat  | .magnitude => p.natAbsend Singlenamespace Costnoncomputable def Log (T : ℕ) := Real.log (T+2 : ℝ) / Real.log 2noncomputable def exponent := (2:ℝ)/5end Costnamespace Singleopen Costvariable {X : Type} (M : Single X)def Access (A : M.Sym) (p q : ℝ) (x : List X) (T : ℕ) : Prop :=  ∀ (h : M.Tag) (l : ℤ), Inside T l →    ∃ s : ℕ, (s:ℝ) ≤ p * (Log T)^q ∧      A.Within (binaryIn x (M.arg T h l)) (M.sensor x h l) send Singleend Fifthsnamespace Fifths.Singleopen Entry Costvariable {X : Type} (M : Single X)theorem capped [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :    ∃ (N : TM X Unit M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧      ∀ (x : List X) (T : ℕ), 2 ≤ T → M.Access A p q x T →        ∃ b : ℕ, N.Within (binaryIn x (fun _ => T)) (M.outcome x T) b ∧          (b:ℝ) ≤ c*(T:ℝ)^exponent*(Log T)^e := by  sorrytheorem unknown [Fintype X] (A : M.Sym) (p q : ℝ) (hp : 1 ≤ p) (_hq : 1 ≤ q) :    ∃ (N : TM X Empty M.Outcome) (e : ℕ) (c : ℝ), 0 < c ∧      ∀ (x : List X), (∀ T, 2 ≤ T → M.Access A p q x T) →        ∀ (t : ℕ), (M.outcome x t).2 = true →          ∃ b, N.Within (files x) (M.outcome x t) b ∧            (b:ℝ) ≤ c*((t:ℝ)+2)^exponent*(Log t)^e := by  sorryend Fifths.Singleend 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.

Simulating One-Tape Time in Two-Fifths-Power Space

Theorem

Fix a deterministic machine with one writable tape and head, a fixed number of read-only input heads, unit movement and fixed origins for all heads, cap-independent symbol functions, and a fixed accessor as above. For every public input x and supplied binary cap T\ge2 for which the access condition holds, its finite-control and halting outcome by time T can be computed deterministically in \softO(T^{2/5}) work-space bits, excluding storage for the read-only input. Simulation time is unrestricted, and the final writable tape need not be materialized. If the access condition holds for (x,T) at every T\ge2, and the machine halts on x after t steps without a supplied running time, its outcome can be computed in \softO((t+2)^{2/5}) work-space bits.

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

Show the TeX

Fix a deterministic machine with one writable tape and head, a fixed
number of read-only input heads, unit movement and fixed origins for
all heads, cap-independent symbol functions, and a fixed accessor as above.
For every public input \(x\) and supplied binary cap \(T\ge2\) for which
the access condition
holds, its finite-control and halting outcome by time \(T\) can be
computed deterministically in \(\softO(T^{2/5})\) work-space bits,
excluding storage for the read-only input. Simulation time is
unrestricted, and the final writable tape need not be materialized.
If the access condition holds for \((x,T)\) at every \(T\ge2\), and
the machine halts on \(x\) after \(t\) steps without a supplied running
time, its outcome can be computed in
\(\softO((t+2)^{2/5})\) work-space bits.

Configuration and file facts

File: lean/ComparatorChallenges/OneTapeSpace.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/Computability/SpaceSimulation/Main.lean, OAI/Computability/SpaceSimulation/Main.lean
Allowed axioms: propext, Classical.choice, Quot.soundThe axioms this configuration allows a proof to use. A replay shows which of them a proof uses.
Imports: Mathlib
Imports from outside Mathlib: None
Local vocabulary: 53 local vocabulary declarations
Lines of Lean, without comments or blank lines: 167
Second proof-verification program (nanoda): Off in OpenAI's configuration.

A shareable summary of this page: the proposed paper match, what the Lean statement expresses, and which reviews are recorded.

Plectis Atlas