Lean formalization in OpenAI math repository (Result 130)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Finite tensor savings and exact Fourier circuits'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 130). The Lean development was not rebuilt locally.