Theoretical computer science · Result 130

Exact Fourier transforms below \(n\log n\)

2 papersLean

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.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

An explicit power saving for the exact discrete Fourier transform

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026,
  author = {{OpenAI}},
  title = {{An explicit power saving for the exact discrete Fourier transform}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026/main.pdf}{OAI:An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026}},
  year = {2026}
}

Finite tensor savings and exact Fourier circuits

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026,
  author = {{OpenAI}},
  title = {{Finite tensor savings and exact Fourier circuits}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026/main.pdf}{OAI:Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

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.

Comparator links

Result	Comparator statement
Subsequential savings for exact Fourier circuits	ExactFourier.lean
Uniform exact DFT and convolution with a power saving	UniformFourier.lean

Scope note on GitHub →