Exact discrete Fourier transform

Compute the exact discrete Fourier transform of a complex vector of any positive length $n$ . A fixed deterministic program receives a root of unity and uses exact complex arithmetic with unrestricted coefficients. Integer values and indices are polynomially bounded. Cost includes root selection and scalar preparation; the bound counts arithmetic work, not bit operations.

Classic bound: $O(n \log n)$ (Cooley and Tukey 1965; Bluestein 1970).

The bound has the form $O(n \log^{1-\kappa} n)$ . $\kappa$ is the saving in the logarithmic exponent; higher is better.

What counts as Claimed: Published results for this problem without a qualifying repository review or Lean proof check.
What counts as Human Verified: This problem has no community repo with a qualifying review rule.
What counts as Lean Verified: A result shows here when we rebuild its Lean proof from source and check, with the Lean kernel, that it proves our exact problem statement. Last checked Oct 10, 4:53 AM PT.

Claimed Human Verified Lean Verified

Rank	Bound	Evidence levelLevel	Player	Date	Link
1	$O(n \log^{1-7.54\cdot 10^{\scriptstyle -4}} n)$	Lean Verified	jacobalansussman and chafreaky @cfky_	Oct 9, 6:43 PM PT	Source	jacobalansussman and chafreaky @cfky_ Oct 9, 6:43 PM PT
2	$O(n \log^{1-7.47\cdot 10^{\scriptstyle -4}} n)$	Claimed	jacobalansussman	Oct 9, 12:00 PM PT	Source	jacobalansussman Oct 9, 12:00 PM PT
3	$O(n \log^{1-6.7\cdot 10^{\scriptstyle -4}} n)$	Claimed	Ryan Shea @ryaneshea	Oct 9, 8:24 AM PT	Source	Ryan Shea @ryaneshea Oct 9, 8:24 AM PT
4	$O(n \log^{1-4.85\cdot 10^{\scriptstyle -4}+\varepsilon} n)$	Claimed	eumemic	Oct 9, 2:34 AM PT	Source	eumemic Oct 9, 2:34 AM PT
5	$O(n \log^{1-7.3\cdot 10^{\scriptstyle -5}} n)$	Claimed	Ryan Shea @ryaneshea	Oct 8, 4:56 PM PT	Source	Ryan Shea @ryaneshea Oct 8, 4:56 PM PT
6	$O(n \log^{1-2\cdot 10^{\scriptstyle -11}+\varepsilon} n)$	Lean Verified	OpenAI	Oct 7, 10:20 PM PT	Source	OpenAI Oct 7, 10:20 PM PT
7	$O(n \log^{1-10^{\scriptstyle -13}} n)$	First breakthrough · Lean Verified	OpenAI	Oct 6	Source	OpenAI Oct 6

$\kappa$ in $O(n \log^{1-\kappa} n)$ , higher is better $\kappa$ in $O(n \log^{1-\kappa} n)$ log scale, higher is better

ClaimedHuman VerifiedLean Verified

First breakthrough

○ strict endpoint

\kappa

(log scale)

\kappa=1:\ O(n)

$\kappa$ in $O(n \log^{1-\kappa} n)$ , higher is better $\kappa$ in $O(n \log^{1-\kappa} n)$ log scale, higher is better

Relevant repos

Ask about Big O Speedrun

Exact discrete Fourier transform

κ\kappaκ in O(nlog⁡1−κn)O(n \log^{1-\kappa} n)O(nlog1−κn), higher is betterκ\kappaκ in O(nlog⁡1−κn)O(n \log^{1-\kappa} n)O(nlog1−κn)log scale, higher is better

Relevant repos iWe list repositories that publish a result for this problem or accept improvements to it. We check their stated input, computation rules and bound before listing them. A listing does not imply that we checked their proof.

$\kappa$ in $O(n \log^{1-\kappa} n)$ , higher is better $\kappa$ in $O(n \log^{1-\kappa} n)$ log scale, higher is better

Relevant repos