VibeMathedMath problems solved with AI
Sign in

The Barker-sequence conjecture: no Barker sequence of length greater than 13

A Barker sequence of length n>1n>1 is a sign sequence a∈{−1,1}na\in\{-1,1\}^n whose aperiodic autocorrelations Ca(t)=∑j=0n−t−1ajaj+tC_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t} satisfy ∣Ca(t)∣≤1|C_a(t)|\le1 for 1≤t<n1\le t<n. Examples exist at lengths 2, 3, 4, 5, 7, 11 and 13. Turyn and Storer (1961) showed that no odd length beyond 13 occurs, and an even length beyond 4 forces all periodic autocorrelations to vanish, that is, a circulant Hadamard matrix of that order. The Barker-sequence conjecture asserts that no Barker sequence of length greater than 13 exists. Is the list {2,3,4,5,7,11,13}\{2,3,4,5,7,11,13\} complete?

Result
Proved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Sequence design; aperiodic autocorrelation
Posed by
Not named in the manuscript; it cites Turyn and Storer (1961) for the odd-length theorem
Year posed
—
Years open
—
Solved
2026-09-23
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
30 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Corollary 1.2: for n>1n>1, a Barker sequence of length nn exists if and only if n∈{2,3,4,5,7,11,13}n\in\{2,3,4,5,7,11,13\}. The new input is the even case, via the circulant Hadamard theorem; the odd case is the classical Turyn-Storer theorem. Section 5 records examples at every listed length. Nothing is claimed about nearly-Barker sequences or the asymptotic merit-factor problem.

What the AI did

The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. This entry is Corollary 1.2 of the circulant Hadamard manuscript (September 23, 2026): the new circulant Hadamard theorem settles the even case, and the odd case is classical (Turyn-Storer; Schmidt-Willms).

Verification

No independent mathematician has checked this yet. Checked here: Corollary 1.2 and Section 5 were read; the even case reduces to Theorem 1.1 by the classical periodic-autocorrelation argument, and the odd case is quoted from Turyn-Storer and Schmidt-Willms. The challenge lean/ComparatorChallenges/EvenBarker.json (solution module OAI.LinearAlgebra.Barker.Main, present at the pinned commit) is not in the formalization catalogue; its statement EvenBarker.lean was read here: a ±1\pm1 integer sequence of positive even length nn with all aperiodic autocorrelations at shifts 0<k<n0<k<n of absolute value at most 1 has n=2n=2 or n=4n=4. This covers the even half, which is the new part; the odd-length classification is not formalized. Not rebuilt here.

Sources

Changelog1 change

Discussion