Episode 179, October 2026

Only orders 1 and 4?

A preprint claims the circulant Hadamard conjecture, and with classical results the complete list of Barker sequences

Covers result 179 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 179: Only orders 1 and 4? The 4 by 4 circulant Hadamard matrix, plus and minus signs in teal and pink, each row the one above shifted one step (our drawing).

6:00. English captions available. The video loads from YouTube when you press play.

Chapters

The claim, in plain words

A Hadamard matrix is a square table of +1s and −1s whose rows are pairwise perpendicular: any two different rows agree in exactly half of their places. A circulant one is built from a single row, each row the one above shifted one step to the right. With four entries there is one, with first row (+, +, +, −), unique up to rotation and sign. In the Fourier picture (ours), a circulant Hadamard row is one whose discrete Fourier transform has the same size, √n, at every frequency. The row sum squared equals n, so n must be a perfect square, and above 1 it must be even; our exhaustive search of every row of every length up to 20 finds only lengths 1 and 4.

As the paper recounts, the conjecture that there are no others beyond order 4 is traditionally attributed to Ryser (1963). Turyn showed in 1965 that any larger order must be 4u² with u odd and not a prime power, so the first order that condition allows is 900; in 2017 Logan and Mossinghoff excluded all but 4,489 integers up to 4 × 10³⁰. Several complete proofs have been claimed before, and the paper lists them without comment. Barker sequences are ±1 sequences whose shifted copies, without wrapping around, overlap with sums of size at most one; they exist at lengths 2, 3, 4, 5, 7, 11 and 13. Turyn and Storer ruled out odd lengths above 13 in 1961 (the paper uses Schmidt and Willms for the exact list), and an even-length Barker sequence longer than 4 would give a circulant Hadamard matrix.

Result 179 is one OpenAI preprint, The circulant Hadamard conjecture (15 pages, dated September 23, 2026). Its Theorem 1.1: “For a positive integer n, a real circulant Hadamard matrix of order n exists if and only if n ∈ {1, 4}.” Its Corollary 1.2: “For an integer n > 1, a Barker sequence of length n exists if and only if n ∈ {2, 3, 4, 5, 7, 11, 13}.” “The new input is the circulant Hadamard theorem for even lengths; the odd-length classification is classical.”

What it doesn’t claim

Not the Hadamard conjecture itself, that some Hadamard matrix exists in every order divisible by 4; the paper does not touch it. Only real entries: complex circulant Hadamard matrices exist in many orders. Only cyclic shifts: over other groups the analogous objects exist; by our count there are no Hadamard (16, 6, 2) difference sets in the cyclic group of order 16, but 192, 192, 448 and 448 in the other four abelian groups of that order. The odd-length Barker classification is cited, not reproved. The paper uses no computer search.

Where it stands

Posted as a preprint: OpenAI, 15 pages, dated September 23, 2026
Peer reviewed: Not yet
Checked in Lean: The circulant theorem and the even-length Barker statement, formalized by OpenAI; not run by us

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statement is the circulant theorem exactly as in the paper, with explicit examples at orders 1 and 4; by our count the proof takes 68 files and 9,496 lines, excluding Mathlib (source). A second statement proves that a Barker sequence of even length has length 2 or 4 (73 files and 9,773 lines in all). The odd-length Barker classification is not formalized. We found no unproved steps by search; we have not rebuilt the proofs. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

One identity. Write the row as a polynomial h in X with Xⁿ = 1. All rows are perpendicular exactly when h h* = n, where h* is the mirror image.
The order is 4u², u odd. In a group-ring form of Turyn’s argument, folding the row in half again and again shows that the order must be four times an odd square.
Four sub-rows. Since 4 and u² share no factor, the cycle splits into a cycle of four and a cycle of u². Split the row into four interleaved sub-rows H₀, …, H₃, set the four-cycle variable to 1, −1 and i, and halve: c, d and g each satisfy x x* = u².
An alternating product. For each set of primes dividing u, evaluate at a character of order p for each prime in the set, and multiply and divide the values over all sets. The product has size one. A character comparison lemma (Turyn compared character values under extra hypotheses), which works because the cyclic group carries exactly the same power of each prime as the norm u², makes it an algebraic integer congruent to one at those primes; by Kronecker’s criterion it is a root of unity, and the congruences make its order odd.
At a prime over two. The sign structure makes the ratios of the products congruent to one, so, by a trick Leung and Schmidt also used, they equal one; comparing first-order terms shows that a unit is congruent to zero, a contradiction. Order 4 escapes because there one of the ratios is i, of even order. (Turyn had already studied the four coset blocks under an extra hypothesis.)

The numbers in the video

Our checks of the order-4 example: H H^T = 4I, the Fourier transform (2, −2i, 2, 2i), and all 8 first rows.
Our exhaustive search of every first row of every order up to 20 (only 1 and 4), and of every Barker sequence up to length 30 (only 2, 3, 4, 5, 7, 11, 13).
Order 36 with the paper’s own decomposition (a case Turyn had already excluded): 108 integer and 432 Gaussian elements of norm 9 on the cycle of 9; none satisfies even the norm identities with the paper’s two congruences. Over the non-cyclic group C₄ × C₃ × C₃, the same search finds 15,552 group-developed sign rows.
Hadamard (16, 6, 2) difference sets in the abelian groups of order 16: 0 in the cyclic group, 192, 192, 448 and 448 in the others.
The Lean count: our count of the import closures.

Read the source

The circulant Hadamard conjecture (PDF), 15 pages.
The Lean scope note.
The collection’s catalog, where this is result 179.

The paper

OpenAI groups related papers into one result; this one has a single paper.

The circulant Hadamard conjecture

Transcript

Read the full script

0:00The question

A Hadamard matrix is a square table of plus and minus ones whose rows are pairwise perpendicular: any two different rows agree in exactly half of their places. A circulant one is built from a single row: each row is the one above, shifted one step to the right. With four entries there is one, up to rotation and sign: plus, plus, plus, minus. In the Fourier picture, which is ours, a circulant Hadamard row is one whose discrete Fourier transform has the same size, the square root of n, at every frequency. Are there more? The row sum squared equals n, so n must be a perfect square, and above one it must be even. Our exhaustive search, over every possible row of every length up to 20, finds only lengths 1 and 4. In the language of difference sets, the minus signs would form a perfectly balanced pattern: every nonzero shift would line up the same number of them. The conjecture that four is the last one is traditionally attributed to Ryser, from his book of 1963. Turyn showed in 1965 that any larger order must be four times the square of an odd number that is not a prime power, so the first order that condition allows is 900. Later number theory excluded much more: in 2017, Logan and Mossinghoff left only 4,489 candidate orders up to 4 × 10³⁰. Several complete proofs have been claimed before; the paper lists them without comment. A related question concerns Barker sequences: plus and minus ones whose shifted copies, without wrapping around, overlap with sums of size at most one. They exist at lengths 2, 3, 4, 5, 7, 11 and 13. Turyn and Storer ruled out odd lengths above 13 in 1961, and an even-length Barker sequence longer than four would give a circulant Hadamard matrix.

1:57The claim

Result 179 is a single OpenAI preprint, 15 pages long, dated September 23, 2026. Its theorem: a real circulant Hadamard matrix of order n exists if and only if n is 1 or 4. Its corollary: a Barker sequence of length greater than one exists exactly at lengths 2, 3, 4, 5, 7, 11 and 13. The new part of the corollary is the even lengths; the odd lengths come from the classical results it cites. Not claimed: the Hadamard conjecture itself, that ordinary Hadamard matrices exist in every order divisible by four; that question is untouched. Only real entries: complex circulant Hadamard matrices exist in many orders. Only cyclic shifts: over other groups the analogous objects do exist. In our search of order 16, there are no such difference sets in the cyclic group, but between 192 and 448 in each of the other four abelian groups of that order. And the paper uses no computer search at all.

3:05How the proof goes

The proof is short, about 6 pages of argument after a classical first step. Write the row as a polynomial in X, with X to the n equal to one. The Hadamard condition becomes a single identity: the polynomial times its mirror image equals n. First, in a group-ring form of Turyn’s argument, folding the row in half again and again shows that the order must be four times an odd square, u squared. Since four and u squared share no factor, the cycle splits into a cycle of four and a cycle of u squared. So split the row into four interleaved sub-rows, and set the four-cycle variable to one, to minus one, and to i. Halving gives three new objects, c, d and g, each of which times its mirror image equals exactly u squared. Next, for each set of primes dividing u, evaluate these objects at a character of order p for each prime in the set, and combine the values in an alternating product, multiplying and dividing over all the sets. Every value has size u, so the product has size one. The key lemma compares character values, as Turyn did under extra conditions, and it works because the cyclic group carries exactly the same power of each prime as the norm u squared. It makes the product an algebraic integer congruent to one at those primes, so by Kronecker’s criterion it is a root of unity, and the congruences make its order odd. Now reduce at a prime lying over two. The plus and minus signs make the ratios of these products congruent to one, and, by a trick Leung and Schmidt also used, a root of unity of odd order that is congruent to one must equal one. Comparing first-order terms then shows that a unit is congruent to zero, a contradiction. Order four escapes because there one of the ratios is i, of even order. In our computation at order 36, a case Turyn had already excluded, the norm identities and the paper’s two congruences already leave no solutions; over a non-cyclic group of the same size, 15,552 sign rows survive.

5:10Where it stands

The preprint is not peer reviewed and has not been revised. OpenAI’s Lean files state the circulant theorem exactly as in the paper, with explicit examples at orders 1 and 4, and prove it in 68 files and about 9,500 lines; a second statement proves that even-length Barker sequences have length 2 or 4. The odd-length Barker classification is not formalized. We found no gaps by search, but we did not run the check. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, the circulant Hadamard conjecture is true: the 4-by-4 table built from plus, plus, plus, minus is as far as it goes, and 13 is the longest Barker sequence.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.