OpenAI claim summary for CS-68

Unrestricted Linear-Circuit Lower Bound for the Discrete Fourier Transform

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 130; 2026-09-25), the asserted result is that exact complex DFTs at every length admit a deterministic arithmetic algorithm with cost $O(n(\log n)^{1-10^{-13}})$, including scalar preparation and indexing in the stated model; In manuscript 2 (family 130; 2026-09-25), the asserted result is that unrestricted complex linear circuits compute exact Fourier transforms with size $o(n\log n)$ along an unbounded sequence of lengths.

Mathematical statement of the claimed result

Manuscript 1.

Let $F_n=(e^{2\pi i jk/n})_{0\le j,k<n}$. The model counts exact complex field operations, preparation of input-independent scalars, and integer/address operations on $O(\log(n+2))$-bit words. A specified root of unity of an effectively computable order $D_*<1024n^3$ is supplied; no finite-precision or bounded-coefficient restriction is imposed. Define \[ m_*=10^6,\quad W_*=2^{71},\quad\Delta=6871402692000000,\quad \theta=\log_{m_*}(m_*-\Delta/W_*)<1. \] One deterministic algorithm is claimed to compute $F_nx$ exactly for every $n\ge1$, $x\in\mathbb C^n$, in \[ O(n(\log n)^{\theta}(\log\log n)^{4-\theta}) =O(n(\log n)^{1-10^{-13}})=o(n\log n) \] time asymptotically, including schedule and scalar construction. The same model, with general field multiplication for pointwise products, computes the linear convolution $c_k=\sum_{r+s=k}a_rb_s$ of two length-$n$ vectors within this cost. The latter is a bilinear arithmetic algorithm, rather than an input-linear circuit.

Manuscript 2.

Let $F_n=(e^{2\pi i jk/n})_{0\le j,k<n}$ and let $L(n)$ be the minimum number of exact complex linear gates computing $F_nx$, where an addition $u+v$, subtraction $u-v$ or multiplication $\lambda u$ by an input-independent scalar each costs one gate; intermediate values can be reused arbitrarily, allowing unrestricted input-independent coefficients, arbitrary intermediate registers and no coefficient-preparation charge. The claim is \[ \liminf_{n\to\infty}\frac{L(n)}{n\log_2n}=0. \] Equivalently, for every $c>0$ and every $N_0\ge2$, there is some $n\ge N_0$ and an exact circuit using fewer than $cn\log_2n$ gates. This gives a subsequence bound in the unrestricted linear-circuit model, not an every-length bit-time algorithm.

Outline of the argument

For manuscript 1 (family 130; 2026-09-25), a fixed two-coordinate network supplies a tensor-axis saving. Exact-width Toeplitz and Fourier factorizations preserve borrowed coordinates, while coprime working lengths, CRT permutations, and chirp convolution extend the saved transform to every requested length.

For manuscript 2 (family 130; 2026-09-25), a finite improvement over the standard tensor-axis matrix-call count is amplified in tensor powers. A price-separation argument guarantees such a saving, and an exact-width Fourier factorization transfers it while charging diagonal scalings and auxiliary operations.

Formal verification

For manuscript 2 (family 130; 2026-09-25), the documented Lean scope is sub-$n\log n$ exact Fourier circuit size on an unbounded sequence of lengths, with scalar gates charged; there is no all-length or bit-complexity guarantee in that declaration.

The selected statement includes the clause used for this problem.

No Lean formalization is listed at this snapshot for manuscript 1 (family 130; 2026-09-25).

The linked family Comparator checks are ExactFourier.lean.

Their named declarations include OAI.ExactFourier.main_theorem.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, An explicit power saving for the exact discrete Fourier transform, 2026-09-25; citation key OAI:An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main, eq:main-bound; Statement source: cor:decimal; Statement source: cor:polynomial-multiplication.
• OpenAI, Finite tensor savings and exact Fourier circuits, 2026-09-25; citation key OAI:Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 130: Lean scope.
• Comparator ExactFourier.json.
• Comparator ExactFourier.lean.
• OpenAI catalogue entry.