Oct 6, 2026
Lean formalization in OpenAI math repository (Result 076)
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 'Asymptotically minimal maxima of real Littlewood polynomials'. We prove that the minimum possible maximum modulus on the unit circle of a polynomial with N consecutive real coefficients in \{-1,1\} is (1+o(1))\sqrt N, as N tends to infinity through all integers. This disproves the real-sign analogue of Erdős's fixed relative-gap conjecture. As a consequence, the largest binary merit factor at length N tends to infinity through all integer lengths, disproving Turyn's conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 076). The Lean development was not rebuilt locally.