Exact Fourier transforms below n log n
Exact Fourier transforms below n log n is the subject of two manuscripts dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). They concern the number of arithmetic operations needed to compute the discrete Fourier transform exactly. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- All-length algorithm. One deterministic algorithm computes the discrete Fourier transform of every length n in O(n(log n)1−δ) operations with δ = 10−13. The model allows exact complex arithmetic, unrestricted coefficients and a supplied root of unity, and it counts scalar preparation and logarithmic-word indexing. The manuscript also states the same bound for exact convolution.
- Exact Fourier circuits. Along an unbounded sequence of lengths, exact circuits compute the discrete Fourier transform with o(n log n) additions, subtractions and scalar multiplications. This refutes the Ω(n log n) lower bound in the unrestricted complex linear-circuit model.
- Sources (openai/math repository, commit
1581d4c): An explicit power saving for the exact discrete Fourier transform and Finite tensor savings and exact Fourier circuits. - Formalization, as described by the repository. The scope note lean/docs/130.md covers both results. The first is the subsequential circuit statement, with comparator ExactFourier.lean. The second gives fixed programs for every positive length that compute the discrete Fourier transform and full convolution exactly, in work O(n(log n)1−10−13), with comparator UniformFourier.lean. The uniform formalization was added in commit
3014888(8 October 2026); the scope note of the initial commitadc7f12listed only the circuit statement. - Companion result. The same finite complex network is used in the collection's manuscript on Integer multiplication below n log n.
Public follow-up work
Several projects improve the saving δ in the same model. The values below are those stated by each source; the projects build on one another and on shared community circuits, so they are not independent.
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | xangma/exact-fourier-circuits | Use (formalization) | A Lean project for the subsequential circuit result, with an exact-arithmetic circuit engine and an explicit finite witness for the saving, plus numerical diagnostics. | The README reports a successful check with Lean 4.34.1, 1,101 declarations depending only on the standard axioms, and AI assistance for later additions. |
| 2026-10-08 | Ryan Shea and credited contributors, shea256/fourier-transform-below-nlogn | Extension (formalization) | A living project transferring improved finite networks from the integer multiplication work to all-length Fourier bounds. Its current result is δ = 0.0012331685, with a Lean proof. | The README reports that the proof passes the official comparator and the Lean and nanoda kernels locally, that leaderboard verification is outstanding, and that the work is AI-assisted. |
| 2026-10-09 | Jacob Sussman, jacobalansussman/wht-power-saving-lean | Extension (formalization) | The discrete Fourier transform of every length, and convolution, with saving 8.762478·10−4 (fourth result, 10 October), stated in OpenAI's challenge file with the exponent replaced; a Walsh–Hadamard transform result with a similar saving. | Lean kernel and comparator runs reported in the README, with the comparator run using a stand-in for its sandbox. The author directed a team of AI agents (Claude) and notes that the proofs have not had a line-by-line human review. |
| 2026-10-09 | eumemic, eumemic/exact-dft-bounds | Extension | O(n(log n)θ(log log n)4−θ) with θ = 1 − 607/1250000, for every length and for exact convolution, by batching the manuscript's recursion. | A paper proof with an exact finite certificate, not formally verified; it depends on the correctness of a community-built finite network. Prepared with substantial assistance from Claude. |
| 2026-10-09 | danadran01/exact-dft-power-saving | Extension (formalization) | Saving 3.2·10−6 by grouped recursion over each edge of the network and new "colour register" networks, as a Lean extension of OpenAI's formalization. | The paper is credited to Claude (Anthropic). The README states that the final theorem uses only the standard axioms. |
| 2026-10-11 | spele1100/exact-dft | Use (implementation) | A component-level reference implementation of the constructions in exact cyclotomic arithmetic. | The README states that it does not reproduce the asymptotic power saving. |
| 2026-10-14 | Oleksandr Pylypenko, cyberdid/fft-power-saving-verification (Zenodo software 10.5281/zenodo.23375601; preprint 10.5281/zenodo.23375871) | Support (computational) | An independent exact and numerical check of the local Fourier compiler in the all-length manuscript. | Software release v1.0.0 and preprint version 1.0 on Zenodo; the README notes that preprint publication does not imply peer review. |
Notes
- The community leaderboard Big O Speedrun records submitted savings for this problem and whether a submission has passed its Lean verifier.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
- The savings above improve a theoretical exponent; they are not measured running times.