Oct 6, 2026
Lean formalization in OpenAI math repository (Result 130)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An explicit power saving for the exact discrete Fourier transform'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 130). The Lean development was not rebuilt locally.