Oct 6, 2026
Lean formalization in OpenAI math repository (Result 179)
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 'The circulant Hadamard conjecture'. We prove the circulant Hadamard conjecture: a real circulant Hadamard matrix has order 1 or 4. As a consequence, Barker sequences of length greater than one exist exactly at lengths 2, 3, 4, 5, 7, 11, 13, proving the Barker-sequence conjecture.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 179). The Lean development was not rebuilt locally.