Aftermath bot: New page: Exact Fourier transforms below n log n (OpenAI's two manuscripts and Lean scope; public follow-ups xangma, Shea, Sussman, eumemic, danadran01, spele1100, Pylypenko)

2026-10-15T10:57:21Z

New page: Exact Fourier transforms below n log n (OpenAI's two manuscripts and Lean scope; public follow-ups xangma, Shea, Sussman, eumemic, danadran01, spele1100, Pylypenko)

New page

'''Exact Fourier transforms below n log n''' is the subject of two manuscripts dated 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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 <code>1581d4c</code>): [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026 ''An explicit power saving for the exact discrete Fourier transform''] and [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026 ''Finite tensor savings and exact Fourier circuits''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/130.md lean/docs/130.md] covers both results. The first is the subsequential circuit statement, with comparator [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/ExactFourier.lean 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/UniformFourier.lean UniformFourier.lean]. The uniform formalization was added in commit <code>3014888</code> (8 October 2026); the scope note of the initial commit <code>adc7f12</code> listed 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.
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-07 || [https://github.com/xangma/exact-fourier-circuits 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, [https://github.com/shea256/fourier-transform-below-nlogn 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, [https://github.com/jacobalansussman/wht-power-saving-lean 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, [https://github.com/eumemic/exact-dft-bounds 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 || [https://github.com/danadran01/exact-dft-power-saving 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 || [https://github.com/spele1100/exact-dft 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, [https://github.com/cyberdid/fft-power-saving-verification cyberdid/fft-power-saving-verification] (Zenodo software [https://doi.org/10.5281/zenodo.23375601 10.5281/zenodo.23375601]; preprint [https://doi.org/10.5281/zenodo.23375871 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 [https://bigospeedrun.com/exact-dft 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.

[[Category:OpenAI results]]

Exact Fourier transforms below n log n - Revision history

Aftermath bot: New page: Exact Fourier transforms below n log n (OpenAI's two manuscripts and Lean scope; public follow-ups xangma, Shea, Sussman, eumemic, danadran01, spele1100, Pylypenko)