∑math20

Combinatorics · Result 179

The circulant Hadamard and Barker-sequence conjectures

1 paperLean

Proves that real circulant Hadamard matrices exist exactly in orders 1 and 4, resolving the circulant Hadamard conjecture. Together with classical Barker-sequence results, this shows that binary sequences whose nontrivial aperiodic autocorrelations have magnitude at most 1 exist at lengths n > 1 exactly when \(n\in\{2,3,4,5,7,11,13\}\).

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of The circulant Hadamard conjecture

The circulant Hadamard conjecture

OpenAI · September 23, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:The-circulant-Hadamard-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{The circulant Hadamard conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-circulant-Hadamard-conjecture-September-23-2026/paper.pdf}{OAI:The-circulant-Hadamard-conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves the circulant Hadamard conjecture in exact form: a real circulant Hadamard matrix of positive order \(n\) exists exactly when \(n=1\) or \(n=4\). Explicit witnesses are supplied for both orders, with no restriction on prime factors.

It also proves the even-length part of the Barker-sequence consequence. A positive even-length sign sequence whose nonzero aperiodic autocorrelations have absolute value at most one must have length \(2\) or \(4\). The paper's classification of odd Barker lengths is outside this selected additional statement.

Comparator links

ResultComparator statement
Classification of circulant Hadamard ordersCirculantHadamard.lean
Classification of positive even Barker lengthsEvenBarker.lean

Scope note on GitHub →