OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Gives a deterministic length-n discrete Fourier transform algorithm using \(O(n(\log n)^{1-\delta})\) operations for every n, with explicit \(\delta=10^{-13}\). The model uses exact complex arithmetic, unrestricted coefficients and a supplied root of unity, and counts scalar preparation and logarithmic-word indexing. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above.Read the assessments
The paper’s main theorem is shown as a possible match to OpenAI’s description. No review confirming the selection is recorded.
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
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
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.
The release does not say which paper theorem its catalogue describes. Both statements above are shown whole: the paper’s main theorem first, then the statement that shares the most wording with the description. The atlas has not reviewed either choice.
Two more possible matches
Corollary 1.2in An explicit power saving for the exact discrete Fourier transform, 25 September 2026.
Theorem 1.1in Finite tensor savings and exact Fourier circuits, 25 September 2026.
Reported proof verification
Two Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
We give a deterministic algorithm that computes the discrete Fourier transform at every length n in \(O(n(\log n)^{1-10^{-13}})\) operations. The model uses exact complex arithmetic, unrestricted coefficients, specified Fourier roots, and unit-cost logarithmic-size indexing; scalar preparation and array organization are included.
We construct exact nonuniform Fourier circuits of size \(o(n\log n)\) along an unbounded sequence of lengths, counting every addition, subtraction, and scalar multiplication. This refutes the \(\Omega(n\log n)\) lower bound in the unrestricted complex linear-circuit model. The construction uses a finite tensor saving: a tensor power of some invertible nonmonomial complex matrix can be computed with fewer matrix calls than the standard tensor-axis algorithm on the same coordinates, when invertible monomial maps are allowed freely between calls.
Two Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
ExactFourier.lean, the release lists it as a main result.
defMainStatement : Prop := ∀ c : ℝ, 0 < c → ∀ N₀ : ℕ, 2 ≤ N₀ → ∃ n : ℕ, N₀ ≤ n ∧ ∃ C : Circuit n, C.Computes (fourierMatrix n) ∧ (C.size : ℝ) < c * (n : ℝ) * Real.logb 2 (n : ℝ)⋮theoremmain_theorem : MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
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
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.
The words they share: arithmetic, bilinear, circuit, complex, computes, construction, convolution, cost, deterministic, exact, including, input, integer, model, multiplication, positive, preparation, root, scalar, total, work.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
UniformFourier.lean, the release lists it as a main result.
defDFTGoal : Prop := ∃ order solve W, DFTProgram order solve W ∧ TimeBounds W⋮theoremtransform_main : DFTGoal := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
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
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: 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.
The formalized result gives exact discrete Fourier transforms with arbitrarily small normalized circuit cost along an unbounded sequence of lengths. For every $c>0$ and every cutoff $N_0\ge2$, some $n\ge N_0$ has a circuit computing the unnormalized DFT with fewer than $cn\log_2 n$ gates. Addition, subtraction, and multiplication by a predetermined complex scalar each cost one gate; diagonal scalings are charged. The result is subsequential, with no all-length, bounded-coefficient, conditioning, or bit-complexity claim.
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$. The synthesis appendix’s extraction, search, and printer uniformization is outside these selected statements.
AI-drafted comparisons, with no recorded human review
Subsequential savings for exact Fourier circuitsExactFourier
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: along an unbounded sequence of lengths, exact DFT circuits with fewer than cn log₂ n gates for every c > 0.
Uniform exact DFT and convolution with a power savingUniformFourier
Unreviewed AI draft: states a paper’s theorem as the paper does. States the power-saving paper’s main theorem with its corollaries: one fixed program computing the DFT at every length, and exact convolution, in O(n(log n)^{1−10^{-13}}) operations.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
Subsequential savings for exact Fourier circuitsExactFourier
Three reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“CERTIFIED”
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
Lemma A.1 of An explicit power saving for the exact discrete Fourier transform, 25 September 2026
Reported by
cert-machine
Method
Exact computation
Their verdict
“NEEDS DATA” Cannot be decided from the release: the specific object the argument relies on is not published.
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
Scientific American (byline not recorded), The most exciting claims from OpenAI’s heap of new proofs, 8 October 2026. Source
The article explains that paper 130 lowers the log n factor in the n log n Fourier transform to a power just below 1, a tiny improvement that nonetheless breaks a barrier of the 1960s.
seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source
Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
Follow-up work by others
danadran01, exact-dft-power-saving, 9 October 2026. Source
A repository claims an exact discrete Fourier transform saving of about 3.2 millionths in the exponent against the manuscript’s one ten-trillionth, verified in Lean; it is a claim by the owner and not independently checked.
Jacob Sussman, jacobalansussman/wht-power-saving-lean: Lean proofs for the DFT and Walsh-Hadamard transform saving, 9 October 2026. Source
Lean-checked saving of 8.76e-4 for the all-length DFT (the five-stage network).
Ryan Shea, shea256/fourier-transform-below-nlogn, 9 October 2026. Source
The project rebuilt the Lean proof of Sussman and Boukhalfa’s five-stage theorem: the release’s UniformFourier statement with the saving raised from 10^-13 to 0.000754736. Its 91 imported OpenAI files are byte-identical at fd4aeeb2. The comparison used Sussman’s Compare.lean rather than OpenAI’s Comparator, and human review is pending.
Ryan Shea, shea256/fourier-transform-below-nlogn, 8 October 2026. Source
A conditional exponent saving for the exact discrete Fourier transform built on the community integer multiplication network, published as an unreviewed research draft with verifiers.
chris1234555, chris1234555/ncc-certificate: Lean certificate that the Li-Li network coding conjecture is false, 7 October 2026. Source
Lean refutation of a consequence of the network coding conjecture using the family 130 DFT circuits.
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a algorithm and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Scientific American (byline not recorded), The most exciting claims from OpenAI’s heap of new proofs, 8 October 2026. Source
Paper 130 reduces the log factor in the fast Fourier transform to a power just under 1, a tiny improvement that breaks a long-standing barrier.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 130The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Address a question raised in an independent assessment
The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method
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.
The challenge statements state the headline as OpenAI wrote it.
Their method
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…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
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.
Re-run through Comparator with Lean’s kernel: accepted (the check took 195 s; peak memory 6.6 GiB).
Date
11 October 2026
Version
at the release’s recorded version
Their method
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.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
10 October 2026
Version
at the release’s recorded version
Their method
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.
Lemma A.1 of An explicit power saving for the exact discrete Fourier transform, 25 September 2026
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
Interface and lemma in build/sections/synthesis.tex lines 18-60 (Lemma syn:local-certificate at lines 39-46), built from the network of build/sections/network.tex (matrix eq. net:C at line 6; Prop. net:finite-interface at line 370; parameters m=10^6, W_*=2^71 at network.tex line 470 and introduction.tex line 71). The 2^b-coordinate word is never printed and is astronomically large.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.