Lean statement

Uniform exact DFT and convolution with a power saving

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.

Theorems selected for verification: OAI.PowerSaving.transform_main OAI.PowerSaving.convolution_main

Lean statement file: UniformFourier.leanShow on the mapFamily 130. 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.

def DFTGoal : Prop := ∃ order solve W, DFTProgram order solve W ∧ TimeBounds W⋮def ConvGoal : Prop := ∃ order solve W, ConvProgram order solve W ∧ TimeBounds W⋮theorem transform_main : DFTGoal := by  sorry⋮theorem convolution_main : ConvGoal := 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.

definition OAI.ExactFourier.zeta line 6

noncomputable def zeta (n : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / (n : ℂ))

structure OAI.PowerSaving.Tape line 51

structure Tape (α : Type u) where  len : ℕ  pos : Fin len → α

definition OAI.PowerSaving.Tape.tab line 60

def tab (n : ℕ) (f : ℕ → α) : Tape α := ⟨n, fun i => f i.val⟩

definition OAI.PowerSaving.Tape.look line 63

def look (v : Tape α) (i : ℕ) (z : α) : α :=  if h : i < v.len then v.pos ⟨i,h⟩ else z

definition OAI.PowerSaving.Tape.set line 74

def set (v : Tape α) (i : ℕ) (x : α) : Tape α :=  ⟨v.len, fun j => if j.val = i then x else v.pos j⟩

definition OAI.PowerSaving.Tape.sow line 77

def sow (len count : ℕ) (z : α) (f : ℕ → ℕ × α) : Tape α :=  iter countwhere  iter : ℕ → Tape α  | 0 => tab len (fun _ => z)  | i+1 => (iter i).set (f i).1 (f i).2

inductive type OAI.PowerSaving.RAM.Paint line 90

inductive Paint  | scalar  | left  | right  | both

inductive type OAI.PowerSaving.RAM.Ty line 96

inductive Ty  | w  | c : Paint → Ty  | p : Ty → Ty → Ty  | a : Ty → Ty

abbreviation OAI.PowerSaving.RAM.sc line 104
```
abbrev sc := c .scalar
```

structure OAI.PowerSaving.RAM.Bill line 121

structure Bill (α : Type u) where  val : α  work : ℕ  peak : ℕ  valid : Prop

definition OAI.PowerSaving.RAM.Bill.word line 139

def word (x : ℕ) : Bill ℕ := ⟨x,1,x,True⟩

inductive type OAI.PowerSaving.RAM.NOp line 157

inductive NOp  | add | sub | mul | div | mod | lt  -- truncated subtraction; compare returns 1 or 0

inductive type OAI.PowerSaving.RAM.Atom line 160

inductive Atom (allow : Bool) : Ty → Ty → Type  | lit {a} (n : ℕ) : Atom allow a w  | int (f : NOp) : Atom allow (p w w) w  | cz (t) {a} : Atom allow a (c t)

Show the remaining 12 lines

  | cone {a} : Atom allow a sc  | add (t) : Atom allow (p (c t) (c t)) (c t)  | sub (t) : Atom allow (p (c t) (c t)) (c t)  | scale (t) : Atom allow (p sc (c t)) (c t)  | inv : Atom allow sc sc  | cross (h : allow = true) :      Atom allow (p (c .left) (c .right)) (c .both)  | id {a} : Atom allow a a  | fst {a b} : Atom allow (p a b) a  | snd {a b} : Atom allow (p a b) b  | len {s} : Atom allow (a s) w  | look {s} : Atom allow (p (a s) w) s

definition OAI.PowerSaving.RAM.NOp.run line 177

noncomputable def NOp.run : NOp → (ℕ × ℕ) → Bill ℕ  | .add, (i,j) => Bill.word (i+j)  | .sub, (i,j) => Bill.word (i-j)  | .mul, (i,j) => Bill.word (i*j)  | .div, (i,j) => Bill.word (i/j) -- includes usual guard (returns zero)  | .mod, (i,j) => Bill.word (i%j) -- like Lean: returns i if j=0  | .lt, (i,j) => Bill.word (if i<j then 1 else 0)

abbreviation OAI.PowerSaving.RAM.Port line 201
```
abbrev Port := Option (Ty × Ty)
```

inductive type OAI.PowerSaving.RAM.Code line 206

inductive Code (allow : Bool) : Port → Ty → Ty → Type  | atom {r s t} (op : Atom allow s t) : Code allow r s t  | comp {r s t u} (f : Code allow r s t) (g : Code allow r t u) : Code allow r s u  | fork {r s t u} (f : Code allow r s t) (g : Code allow r s u) : Code allow r s (p t u)

Show the remaining 11 lines

  | ifz {r s t} (q : Code allow r s w) (f g : Code allow r s t) : Code allow r s t  | loop {r s t} (n : Code allow r s w) (init : Code allow r s t)      (body : Code allow r (p s (p w t)) t) : Code allow r s t  | tab {r s t} (n : Code allow r s w)      (body : Code allow r (p s w) t) : Code allow r s (a t)  | sow {r s t} (n count : Code allow r s w)      (body : Code allow r (p s w) (p w t)) : Code allow r s (a t)  | importClosed {r s t} (f : Code allow none s t) : Code allow r s t  | call {s t} : Code allow (some (s,t)) s t  | descend {r s t} (base : Code allow none s t)      (body : Code allow (some (s,t)) s t) : Code allow r (p w s) t

abbreviation OAI.PowerSaving.RAM.Prog line 251

abbrev Prog (allow : Bool) (s t : Ty) := Code allow none s t

definition OAI.PowerSaving.paperM line 264
```
def paperM : ℝ := 1000000
```

definition OAI.PowerSaving.paperW line 265

def paperW : ℝ := ((2 : ℕ) : ℝ) ^ (71:ℕ)

definition OAI.PowerSaving.paperDelta line 266
```
def paperDelta : ℝ := 6871402692000000
```

definition OAI.PowerSaving.paperMultiplier line 267

def paperMultiplier := paperM - paperDelta / paperW

definition OAI.PowerSaving.theta line 268

def theta : ℝ := Real.log paperMultiplier / Real.log paperM

definition OAI.PowerSaving.decimalExponent line 269

def decimalExponent : ℝ := 1 - 1/(10^(13:ℕ))

definition OAI.PowerSaving.paperTime line 271

def paperTime (n : ℕ) : ℝ :=  (n:ℝ) * (Real.log (n:ℝ)) ^ theta * (Real.log (Real.log (n:ℝ))) ^ (4-theta)

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

Possible paper match, with no recorded review

No paper statement clearly matched the Lean wording. Statement Map, the program that collects Atlas’s source records, selected this possible match using words in OpenAI’s catalogue and Lean note. No review of whether the statements mean the same thing is recorded.

Shared with the catalogue’s wording or OpenAI’s note, none of them matched in the Lean text: arithmetic, bilinear, circuit, complex, computes, construction, convolution, cost and 13 more.

Statements in An explicit power saving for the exact discrete Fourier transform come first because the release’s name for this Lean statement shares words with that paper’s title.

Corollary 1.3 of An explicit power saving for the exact discrete Fourier transform

Corollary (Exact convolution and polynomial multiplication)

There is a single deterministic algorithm which, for every positive integer n and every a,b\in\C^n, computes the linear convolution

\begin{gathered}c_k=\sum_{\substack{0\le r,s<n\\r+s=k}}a_rb_s, \qquad 0\le k\le 2n-2.\end{gathered}

Equivalently, it multiplies two complex polynomials of degree less than n. In the exact complex field-operation, specified-root, and address cost model above, with general field multiplication permitted for the pointwise products, the total running time, including scalar preparation, schedule construction, padding, and index work, is

O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right) \qquad(n\to\infty),

and hence is eventually O(n(\log n)^{1-10^{-13}}). This is a bilinear arithmetic algorithm, not an input-linear circuit: its pointwise products multiply a value linear in a by a value linear in b.

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

Show the TeX

There is a single deterministic algorithm which, for every positive integer
$n$ and every $a,b\in\C^n$, computes the linear convolution
\[
 c_k=\sum_{\substack{0\le r,s<n\\r+s=k}}a_rb_s,
 \qquad 0\le k\le 2n-2.
\]
Equivalently, it multiplies two complex polynomials of degree less than $n$.
In the exact complex field-operation, specified-root, and address cost model
above, with general field multiplication permitted for the pointwise products,
the total running time, including scalar preparation, schedule construction,
padding, and index work, is
\[
 O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right)
 \qquad(n\to\infty),
\]
and hence is eventually $O(n(\log n)^{1-10^{-13}})$.
This is a bilinear arithmetic algorithm, not an input-linear circuit: its
pointwise products multiply a value linear in $a$ by a value linear in $b$.

Other possible paper matches, closest wording first

Theorem A.4 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: instruction, canonical, pi, exp, paper, executed and 17 more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: indices, deterministic and model.
Theorem 1.1 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: zeta, positive, construction, theta, work, computes and seven more. Found in the paper’s title, which its main theorem states: transform and fourier. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: exactly, deterministic and model.
Proposition 3.1 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: primitive, exponent, needs, input, counting, programs and ten more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: coefficients, unity, uniform, remaining, power, arithmetic and two more.
Theorem 2.6 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: initialization, length, array, construction, bound, theta and six more. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: arithmetic and deterministic.
Proposition 4.2 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: max, array, operations, theta, work, roots and six more.
Corollary 1.2 of An explicit power saving for the exact discrete Fourier transform. Words of the Lean statement, its names split into words, that also appear in the theorem: length, transform, computable, time and log. Shared only with the release’s name for the Lean statement or OpenAI’s note on it: model.

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 10 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 130’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: UniformFourier.transform_main (DFTGoal) states that one fixed pair of closed RAM programs (order, solve) outputs dft n x exactly for every n > 0 and every x, with total work including root-order selection (d.work) and scalar preparation at most W n, where W =O n(log n)^(1−10^-13) (also the paper's θ-bound and o(n log n)); unfolding DFTGoal, DFTProgram and TimeBounds is the only step, and convolution_main likewise states Corollary 1.3. ExactFourier is the separate subsequential circuit result (for each c and N₀ some n ≥ N₀ has an exact circuit with fewer than c n log₂ n gates), which is the other paper's theorem and not the headline claim.
Definitions the group asks readers to compare with the paper: UniformFourier RAM model (Tape, Bill, Atom, Code, Code.run, Prog, run): bespoke typed point-free RAM with unit-cost exact complex field operations and unit-cost word operations; the meaning of 'O(...)' rests entirely on its cost semantics. I found no undercharging: every Code node and Atom pays at least 1, tab/sow pay 1+len, loops and bounded descents pay per iteration/level, and arrays are never copied for free ; UniformFourier.DFTProgram / ConvProgram: the program itself selects the root order d = run order n (0 < d < 1024 n³, its work counted) and then receives root d := ExactFourier.zeta d for free; the target is dft n with ζ_n, and every scalar the program can form lies in ℚ(ζ_d), so d must give ζ_n ∈ ℚ(ζ_d) (n | d, or d odd and n | 2d); matches the paper's 'specified root ζ_{D_*}, D_* < 1024 n³' ; UniformFourier Atom set: the only complex constants are 0 (cz) and 1 (cone); every other scalar must be prepared from the supplied root by counted add/sub/scale/inv on scalar registers; data registers (Paint.left/right/both) cannot become scalars or integers, and ifz tests only integers, so control flow is data-independent; 'cross' (data × data) exists only when allow = true (convolution), and only left × right ↦ both ; UniformFourier Bill.valid (a Prop): the side condition that every inv has a nonzero argument on the executed path; DFTProgram and ConvProgram require d.valid and result.valid, so division by zero is excluded rather than tested ; UniformFourier cap := (n+2)^cBound with ∃ cBound: forces work, root order and every produced integer (peak) to be polynomial in n, i.e. O(log n)-bit words; this is the 'logarithmic-word indexing' of the summary ; UniformFourier TimeBounds: W =O paperTime ∧ W =O decimalTime ∧ W =o nlogn with natural logs; asymptotic only (finitely many n are constrained only by correctness and cap); paperTime uses the paper's constants m = 10^6, W_* = 2^71, Δ = 6871402692000000 and θ = log(m − Δ/W_*)/log m; decimalTime n = n (log n)^(1 − 10^-13) ; UniformFourier dft / conv: dft n x j = Σ_k ζ_n^(jk) x_k with ζ_n = exp(+2πi/n) (unnormalized, same sign convention as the paper's F_n); conv is the full linear convolution on Fin (2n−1) ; ExactFourier Gate / Program / Circuit: linear scalar DAG with n inputs, an extra constant 0, free reuse and fan-out, outputs naming any available value (permutations free), and scale (c : ℂ) with arbitrary complex c at cost one; coefficient generation is uncharged (nonuniform); standard for the paper's model ; ExactFourier MainStatement: subsequential (∃ n ≥ N₀ for each c and N₀), not an all-length bound; this is the intended statement of the finite-tensor paper's thm:main
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

“A separate uniform formalization gives fixed deterministic programs for every positive length $n$, computing the canonical discrete Fourier transform and the full convolution of two length-$n$ complex vectors exactly. Their work is $O(n(\log n)^{1-10^{-13}})=o(n\log n)$, including root-order selection and scalar preparation. The chosen root of unity is supplied; the model permits exact complex arithmetic and unrestricted coefficients, while integer values and indices remain polynomially bounded in $n$.”
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

336 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: 271 to its own declarations, 39 to Mathlib’s documentation. 58 declared names also link to the same declaration in OpenAI’s library. 3 identifiers stay plain because they resolve to no single declaration: variables Lean binds automatically, notation, or names the scan of the pinned sources did not find. OpenAI uses Mathlib version d13f23b. The linked documentation describes the current version, so names that have since changed may be missing there.

import Mathlibnamespace OAInamespace ExactFouriernoncomputable def zeta (n : ℕ) : ℂ := Complex.exp (2 * Real.pi * Complex.I / (n : ℂ))end ExactFourier/-!# Exact scalar and index RAM used for the algorithmFinite, first-order, expression/program syntax. Arrays below are random-access arrays ofregisters (an array-valued register holds its address). An expression building an array usesa fresh array; `sow` builds by a loop of writes instead of a loop supplying consecutiveentries. Programs have their usual sequential stack evaluation. Evaluation here records work(including stack, index and array work), the high water mark on produced/logically looped-overinteger values (addresses *within* arrays are integers too), the value, and the side conditionrequired along the executed path (in particular no division by zero). The charged units ofwork are constant time; as usual constant rescalings between ways to charge a fixed numberof scalar or address operations are immaterial.Enough address bits must be provided BOTH for the integer high water mark (and inputs), ANDfor the work bound together with input size, as will be required in the theorem. Indeed weuse the particularly simple RAM convention where temporaries aren't reused: one work unit canleave at most a constant number of cells (stack, pairs or array cells); whenever many arrayentries are made their number is charged. So a constant number of words of those sizes alsosuffices for arena addresses. Nothing charges constant work for changing an already publishedarray to a different array as a whole. Register and stack layouts, and the convention whetherregisters hold pairs or addresses of pairs, only have constant factors (the program is fixed).Scalar and data field registers are separated. Tests and loop/request sizes are on nonnegativeinteger registers. There is no instruction for an arbitrary complex constant. A suppliedspecified root will be an input. Divisions are on prepared scalars; valid runs require everysuch denominator nonzero; the side condition is *not* a test performed by the algorithm.The Bool mode on the syntax allows or prohibits general products (two-input convolutionversus the transform); even when allowed we use separate register kinds before and afterthe bilinear products.Definitions are mathematical operation-count semantics, not a model of running Lean code.E.g. a function on Fin n represents the n cells of a random-access array, not a functionclosure at runtime.-/namespace PowerSavinguniverse u vvariable {α : Type u} {β : Type v}/-- Register arrays. -/structure Tape (α : Type u) where  len : ℕ  pos : Fin len → αnamespace Tapedef empty (α : Type u) : Tape α := ⟨0, Fin.elim0⟩/-- Materialized array. -/def tab (n : ℕ) (f : ℕ → α) : Tape α := ⟨n, fun i => f i.val⟩/-- Read with fixed out of bounds default. -/def look (v : Tape α) (i : ℕ) (z : α) : α :=  if h : i < v.len then v.pos ⟨i,h⟩ else z@[simp] theorem look_of_lt (v : Tape α) (z : α) {i} (h : i < v.len) :    v.look i z = v.pos ⟨i,h⟩ := by simp [look, h]@[simp] theorem look_of_le (v : Tape α) (z : α) {i} (h : v.len ≤ i) :    v.look i z = z := by simp [look, Nat.not_lt.mpr h]/-- Semantics of a write into fresh storage; out-of-range writes are ignored. Only used  during construction, never a whole-tape functional update instruction. -/def set (v : Tape α) (i : ℕ) (x : α) : Tape α :=  ⟨v.len, fun j => if j.val = i then x else v.pos j⟩def sow (len count : ℕ) (z : α) (f : ℕ → ℕ × α) : Tape α :=  iter countwhere  iter : ℕ → Tape α  | 0 => tab len (fun _ => z)  | i+1 => (iter i).set (f i).1 (f i).2def map (f : α → β) (v : Tape α) : Tape β := ⟨v.len, fun i => f (v.pos i)⟩end Tapenamespace RAMinductive Paint  | scalar  | left  | right  | bothinductive Ty  | w  | c : Paint → Ty  | p : Ty → Ty → Ty  | a : Ty → Tyopen Tyabbrev sc := c .scalar@[reducible] def Ty.T : Ty → Type  | w => ℕ  | c _ => ℂ  | p s b => s.T × b.T  | a b => Tape b.Tnoncomputable def Ty.blank : (t : Ty) → t.T  | w => 0  | c _ => 0  | p s t => (s.blank, t.blank)  | a b => Tape.empty b.T/-- One basic work unit below pays for O(1) primitive RAM operations; includes loop and  stack overhead. `peak` tracks produced/needed integer quantities beyond inputs  (total allocation for stack and array bases is covered separately by work). -/structure Bill (α : Type u) where  val : α  work : ℕ  peak : ℕ  valid : Propnamespace Bill/-- Charge some work and optionally a new word bound. -/def pay (b : Bill α) (n : ℕ) (m : ℕ) : Bill α :=  ⟨b.val, b.work+n, max b.peak m, b.valid⟩/-- Both computations are evaluated. -/def pass (b : Bill α) (f : α → Bill β) : Bill β :=  let d := f b.val  ⟨d.val, b.work+d.work, max b.peak d.peak, b.valid ∧ d.valid⟩def one (x : α) : Bill α := ⟨x,1,0,True⟩def word (x : ℕ) : Bill ℕ := ⟨x,1,x,True⟩/-- Execute f 0 through f (n-1), iterating an accumulator. -/def steps (init : α) (f : ℕ → α → Bill α) : ℕ → Bill α  | 0 => Bill.one init  | i+1 => ((steps init f i).pass (f i)).pay 1 (i+1)/-- Build Tape len by count writes (initialized with a blank z). -/def sow (len count : ℕ) (z : α) (f : ℕ → Bill (ℕ × α)) : Bill (Tape α) :=  (steps (Tape.tab len (fun _ => z))    (fun i v => (f i).pass (fun s => one (v.set s.1 s.2))) count).pay (1+len) len/-- Build Tape len. As for sow we can first allocate then perform writes. -/def tab (len : ℕ) (z : α) (f : ℕ → Bill α) : Bill (Tape α) :=  sow len len z (fun i => (f i).pass (fun y => one (i,y)))end Billinductive NOp  | add | sub | mul | div | mod | lt  -- truncated subtraction; compare returns 1 or 0inductive Atom (allow : Bool) : Ty → Ty → Type  | lit {a} (n : ℕ) : Atom allow a w  | int (f : NOp) : Atom allow (p w w) w  | cz (t) {a} : Atom allow a (c t)  | cone {a} : Atom allow a sc  | add (t) : Atom allow (p (c t) (c t)) (c t)  | sub (t) : Atom allow (p (c t) (c t)) (c t)  | scale (t) : Atom allow (p sc (c t)) (c t)  | inv : Atom allow sc sc  | cross (h : allow = true) :      Atom allow (p (c .left) (c .right)) (c .both)  | id {a} : Atom allow a a  | fst {a b} : Atom allow (p a b) a  | snd {a b} : Atom allow (p a b) b  | len {s} : Atom allow (a s) w  | look {s} : Atom allow (p (a s) w) snoncomputable def NOp.run : NOp → (ℕ × ℕ) → Bill ℕ  | .add, (i,j) => Bill.word (i+j)  | .sub, (i,j) => Bill.word (i-j)  | .mul, (i,j) => Bill.word (i*j)  | .div, (i,j) => Bill.word (i/j) -- includes usual guard (returns zero)  | .mod, (i,j) => Bill.word (i%j) -- like Lean: returns i if j=0  | .lt, (i,j) => Bill.word (if i<j then 1 else 0)noncomputable def Atom.run {allow a b} : Atom allow a b → a.T → Bill b.T  | .lit n, _ => Bill.word n  | .int f, x => f.run x  | .cz _, _ => Bill.one 0  | .cone, _ => Bill.one 1  | .add _, (x,y) => Bill.one (x+y)  | .sub _, (x,y) => Bill.one (x-y)  | .scale _, (x,y) => Bill.one (x*y)  | .inv, x => ⟨x⁻¹,1,0,x ≠ 0⟩  | .cross _, (x,y) => Bill.one (x*y)  | .id, x => Bill.one x  | .fst, x => Bill.one x.1  | .snd, x => Bill.one x.2  | .len, x => Bill.word x.len  | @Atom.look _ s, (x,i) => Bill.one (x.look i s.blank)abbrev Port := Option (Ty × Ty)/-- `call` is internal for bounded recursion; a program has Port = none. `loop`, `tab`  and `sow` retain the input to access parameters in the body. `descend` sets up bounded  recursion, reading fuel and initial argument. -/inductive Code (allow : Bool) : Port → Ty → Ty → Type  | atom {r s t} (op : Atom allow s t) : Code allow r s t  | comp {r s t u} (f : Code allow r s t) (g : Code allow r t u) : Code allow r s u  | fork {r s t u} (f : Code allow r s t) (g : Code allow r s u) : Code allow r s (p t u)  | ifz {r s t} (q : Code allow r s w) (f g : Code allow r s t) : Code allow r s t  | loop {r s t} (n : Code allow r s w) (init : Code allow r s t)      (body : Code allow r (p s (p w t)) t) : Code allow r s t  | tab {r s t} (n : Code allow r s w)      (body : Code allow r (p s w) t) : Code allow r s (a t)  | sow {r s t} (n count : Code allow r s w)      (body : Code allow r (p s w) (p w t)) : Code allow r s (a t)  | importClosed {r s t} (f : Code allow none s t) : Code allow r s t  | call {s t} : Code allow (some (s,t)) s t  | descend {r s t} (base : Code allow none s t)      (body : Code allow (some (s,t)) s t) : Code allow r (p w s) t@[reducible] def Handler : Port → Type  | none => Unit  | some (s,t) => s.T → Bill t.Tdef depthRun (base : α → Bill β)    (step : (α → Bill β) → (α → Bill β)) : ℕ → α → Bill β  | 0, x => (base x).pay 1 0  | n+1, x => (step (depthRun base step n) x).pay 1 (n+1)noncomputable def Code.run {allow r s t} : Code allow r s t → Handler r → s.T → Bill t.T  | .atom op, _, x => op.run x  | .comp f g, h, x => ((f.run h x).pass (g.run h)).pay 1 0  | .fork f g, h, x => (f.run h x).pass (fun y => (g.run h x).pass (fun z => Bill.one (y,z)))  | .ifz q f g, h, x => ((q.run h x).pass (fun y =>      if (y : ℕ) = 0 then f.run h x else g.run h x)).pay 1 0  | .loop n init body, h, x =>      ((n.run h x).pass (fun l => (init.run h x).pass (fun y =>        Bill.steps y (fun i z => body.run h (x,(i,z))) l))).pay 1 0  | @Code.tab _ _ _ t n body, h, x =>      ((n.run h x).pass (fun l =>        Bill.tab l t.blank (fun i => body.run h (x,i)))).pay 1 0  | @Code.sow _ _ _ t n count body, h, x =>      ((n.run h x).pass (fun l => (count.run h x).pass (fun k =>        Bill.sow l k t.blank (fun i => body.run h (x,i))))).pay 1 0  | .importClosed f, _, x => (f.run () x).pay 1 0  | .call, h, x => (h x).pay 1 0  | .descend base step, _, (k,x) =>      (depthRun (base.run ()) (step.run) k x).pay 1 kabbrev Prog (allow : Bool) (s t : Ty) := Code allow none s tnoncomputable abbrev run {allow s t} (f : Prog allow s t) (x : s.T) : Bill t.T :=  f.run () xend RAMend PowerSavingnamespace PowerSavingnoncomputable sectionopen RAM RAM.Ty Filter Asymptoticsdef paperM : ℝ := 1000000def paperW : ℝ := ((2 : ℕ) : ℝ) ^ (71:ℕ)def paperDelta : ℝ := 6871402692000000def paperMultiplier := paperM - paperDelta / paperWdef theta : ℝ := Real.log paperMultiplier / Real.log paperMdef decimalExponent : ℝ := 1 - 1/(10^(13:ℕ))def paperTime (n : ℕ) : ℝ :=  (n:ℝ) * (Real.log (n:ℝ)) ^ theta * (Real.log (Real.log (n:ℝ))) ^ (4-theta)def decimalTime (n : ℕ) : ℝ := (n:ℝ) * (Real.log (n:ℝ)) ^ decimalExponentdef nlogn (n : ℕ) : ℝ := (n:ℝ) * Real.log (n:ℝ)abbrev root := ExactFourier.zetaabbrev Vec (n : ℕ) := Fin n → ℂdef dft (n : ℕ) (x : Vec n) : Vec n :=  fun j => ∑ k, (root n) ^ (j.val*k.val) * x kdef conv (n : ℕ) (x y : Vec n) : Vec (2*n-1) :=  fun k => ∑ r : Fin n, ∑ s : Fin n, if r.val+s.val=k.val then x r*y s else 0abbrev dftInKind := p w (p sc (a (c Paint.left)))abbrev dftOutKind := a (c Paint.left)abbrev convInKind := p w (p sc (p (a (c Paint.left)) (a (c Paint.right))))abbrev convOutKind := a (c Paint.both)def DFTProgram (order : Prog false w w) (solve : Prog false dftInKind dftOutKind)    (W : ℕ → ℕ) : Prop :=  ∃ cBound : ℕ, ∀ n : ℕ, 0<n →    let cap := (n+2)^cBound    let d := run order n    W n + 10*(n+2) ≤ cap ∧ d.peak ≤ cap ∧ d.valid ∧    0 < d.val ∧ d.val < 1024*n^3 ∧ d.val ≤ cap ∧    ∀ x : Vec n,      let result := run solve (n, root d.val, (⟨n,x⟩ : Tape ℂ))      result.valid ∧ result.peak ≤ cap ∧ d.work+1+result.work ≤ W n ∧      result.val = (⟨n, dft n x⟩ : Tape ℂ)def ConvProgram (order : Prog false w w) (solve : Prog true convInKind convOutKind)    (W : ℕ → ℕ) : Prop :=  ∃ cBound : ℕ, ∀ n : ℕ, 0<n →    let cap := (n+2)^cBound    let d := run order n    W n + 10*(n+2) ≤ cap ∧ d.peak ≤ cap ∧ d.valid ∧    0 < d.val ∧ d.val < 1024*(2*n-1)^3 ∧ d.val ≤ cap ∧    ∀ x y : Vec n,      let result := run solve (n, root d.val, (⟨n,x⟩ : Tape ℂ),(⟨n,y⟩ : Tape ℂ))      result.valid ∧ result.peak ≤ cap ∧ d.work+1+result.work ≤ W n ∧      result.val = (⟨2*n-1, conv n x y⟩ : Tape ℂ)def TimeBounds (W : ℕ → ℕ) : Prop :=  let W' := fun n : ℕ => (W n : ℝ)  W' =O[atTop] paperTime ∧ W' =O[atTop] decimalTime ∧ W' =o[atTop] nlogndef DFTGoal : Prop := ∃ order solve W, DFTProgram order solve W ∧ TimeBounds Wdef ConvGoal : Prop := ∃ order solve W, ConvProgram order solve W ∧ TimeBounds W/-- One fixed program computes every positive-length canonical DFT, including preparation. -/theorem transform_main : DFTGoal := by  sorry/-- One fixed bilinear program computes convolution with the same asymptotic bounds. -/theorem convolution_main : ConvGoal := by  sorryendend PowerSavingend 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.

Finite tensor savings and exact Fourier circuits

Theorem

In this model,

\liminf_{n\to\infty}\frac{L(n)}{n\log_2 n}=0.

Equivalently, for every c>0 and every integer N_0\ge2, there is an integer n\ge N_0 and an exact circuit for F_n with fewer than c n\log_2 n gates.

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

Show the TeX

In this model,
\[
 \liminf_{n\to\infty}\frac{L(n)}{n\log_2 n}=0.
\]
Equivalently, for every $c>0$ and every integer $N_0\ge2$, there is an
integer $n\ge N_0$ and an exact circuit for $F_n$ with fewer than
$c n\log_2 n$ gates.

An explicit power saving for the exact discrete Fourier transform

Theorem

There is a single deterministic algorithm which, for every positive integer n and every x\in\C^n, computes F_nx exactly. In the model above, including scalar preparation, schedule construction, and index work, its running time is

O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right)

as n\to\infty. It suffices to supply the specified root \zeta_{D_*} for an explicitly computable integer D_*<1024n^3.

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

Show the TeX

There is a single deterministic algorithm which, for every positive integer $n$ and every $x\in\C^n$, computes $F_nx$ exactly. In the model above, including scalar preparation, schedule construction, and index work, its running time is
\begin{equation}
 O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right)
\end{equation}
as $n\to\infty$. It suffices to supply the specified root $\zeta_{D_*}$ for an explicitly computable integer $D_*<1024n^3$.

Corollary

In the same model, the transform is computable at every length in

O\!\left(n(\log n)^{1-10^{-13}}\right)=o(n\log n)

time.

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

Show the TeX

In the same model, the transform is computable at every length in
\[
 O\!\left(n(\log n)^{1-10^{-13}}\right)=o(n\log n)
\]
time.

Corollary (Exact convolution and polynomial multiplication)

There is a single deterministic algorithm which, for every positive integer n and every a,b\in\C^n, computes the linear convolution

\begin{gathered}c_k=\sum_{\substack{0\le r,s<n\\r+s=k}}a_rb_s, \qquad 0\le k\le 2n-2.\end{gathered}

O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right) \qquad(n\to\infty),

and hence is eventually O(n(\log n)^{1-10^{-13}}). This is a bilinear arithmetic algorithm, not an input-linear circuit: its pointwise products multiply a value linear in a by a value linear in b.

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

Show the TeX

There is a single deterministic algorithm which, for every positive integer
$n$ and every $a,b\in\C^n$, computes the linear convolution
\[
 c_k=\sum_{\substack{0\le r,s<n\\r+s=k}}a_rb_s,
 \qquad 0\le k\le 2n-2.
\]
Equivalently, it multiplies two complex polynomials of degree less than $n$.
In the exact complex field-operation, specified-root, and address cost model
above, with general field multiplication permitted for the pointwise products,
the total running time, including scalar preparation, schedule construction,
padding, and index work, is
\[
 O\!\left(n(\log n)^\theta(\log\log n)^{4-\theta}\right)
 \qquad(n\to\infty),
\]
and hence is eventually $O(n(\log n)^{1-10^{-13}})$.
This is a bilinear arithmetic algorithm, not an input-linear circuit: its
pointwise products multiply a value linear in $a$ by a value linear in $b$.

Configuration and file facts

File: lean/ComparatorChallenges/UniformFourier.lean
OpenAI’s Lean catalogue: OpenAI lists this as a main result in its Lean catalogue.
Solution module: OAI/Computability/FourierTransform/Main.lean, OAI/Computability/FourierTransform/Main.lean
Allowed axioms: propext, Quot.sound, Classical.choiceThe 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: 54 local vocabulary declarations
Lines of Lean, without comments or blank lines: 198
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