The circulant Hadamard conjecture

Formalization

• OpenAI, Lean scope note: The circulant Hadamard and Barker-sequence conjectures (openai/math release, 2026-10-06). The release's Lean development proves that real circulant Hadamard matrices of positive order exist exactly for n = 1, 4 (with explicit witnesses) and that even-length Barker sequences have length 2 or 4; the odd-length Barker classification is outside the formalized scope. [family-level]
• mo271, feat: mark problems solved in the OpenAI math release and link formal proofs (google-deepmind/formal-conjectures PR #6898, merged 2026-10-11). Marks circulant_hadamard_conjecture (statement n ≤ 4) as research solved and links the release's theorem OAI.CirculantHadamard.exists_iff_order_one_or_four, absorbing PR #6897; in a review, anxkhn reports compiling a bridge to the repository's IsHadamard' statement and checking axioms, without running Comparator.
• anxkhn, fix(Arxiv/CirculantHadamard): link the OpenAI formal proof (formal-conjectures PR #6897, 2026-10-07, closed in favour of #6898; see also issue #6896). Proposes a Lean bridge from the release theorem to the repository statement; reviewer bocowgill confirmed the implication conditional on the classification theorem and noted that "independent verification of the external proof remains outstanding."
• anxkhn, BridgeCirculant.lean (GitHub Gist, 2026-10-09). The bridge imports the release's circulant Hadamard theorem and derives the Formal Conjectures statement using a copied Hadamard predicate; the author reports checking it with Lean 4.34.1 at a pinned OpenAI commit.
• The Formal Conjectures Authors, CirculantHadamard.lean (Formal Conjectures, 2026). Formalizes the conjecture as an order bound of four and proves an order-four example; the general bound was marked research open with a sorry in the inspected version.
• mo271, Arxiv/2104.00502/BarkerSequence: barker_conjecture is true (formal-conjectures issue #6917, opened 2026-10-07, open). Proposes marking the Barker conjecture solved on the basis of Corollary 1.2, noting that only the even-length case is formalized in the release and the odd-length classification is in the paper only.
• JD Jones, ob-lean: Barker sequences of odd length have length 1, 3, 5, 7, 11 or 13 (GitHub; Palomar entry PALOMAR-2026-10-19-000015, 2026-10-19). An independent Lean 4 formalization of the Schmidt–Willms odd-length classification which, taking the release's theorems even_length_eq_two_or_four and exists_iff_order_one_or_four as explicit hypotheses, derives the full list of Barker lengths conditionally.

Related prior literature mentioned by others

• Jürgen Willms, Counterexamples to Theorem 1 of Turyn's and Storer's Paper "On Binary Sequences" (arXiv:1404.4833, 2014). Cited in the ob-lean repository and its Palomar entry as showing that the Turyn–Storer odd-length argument relies on a false Theorem 1; the manuscript cites Turyn–Storer for odd-length nonexistence and relies on the later Schmidt–Willms proof for the exact list.
• nellore and Rachel Ward (rward314), add references to the circulant Hadamard write-up (mathcommunity/oai-math-revised PR #1, merged 2026-10-18). Adds an introductory paragraph and the references Johnsen 1964, Brualdi 1965 and Newman 1963 on the early settlement of the symmetric circulant case, now in the community version's bibliography.

Possibly relevant literature (found by the agent, not checked)

• Barry Hurley, Paul Hurley, Ted Hurley, The Hadamard circulant conjecture (arXiv:1109.0748, 2011; related to Bull. London Math. Soc., doi:10.1112/blms/bdq112). An earlier claimed proof of the same conjecture that is not among the claimed proofs listed in the manuscript's "Context and prior work".
• Robert Craigen, Jonathan Jedwab, Comment on revised version of "The Hadamard circulant conjecture" (arXiv:1111.3437, 2011). States that the revised Hurley–Hurley–Hurley claimed proof is mistaken; relevant to the manuscript's survey of earlier claimed proofs.
• Peter Borwein, Michael J. Mossinghoff, Wieferich pairs and Barker sequences, II (LMS J. Comput. Math. 17 (2014); arXiv:1306.0045). Gives computational lower bounds and remaining candidate lengths for long Barker sequences, which Corollary 1.2 would cover; not in the manuscript's bibliography.
• Teodor Banica, Ion Nechita and Jean-Marc Schlenker, Analytic aspects of the circulant Hadamard conjecture (arXiv:1212.3589; Annales mathématiques Blaise Pascal 21, 2014). Studies an analytic functional whose equality case characterizes rescaled circulant complex Hadamard matrices, a spectral approach related to the manuscript's circulant orthogonality claim.

Digests and expositions

• Open Mathematics Courses, Circulant Hadamard matrices (undated; accessed 2026-10-21). Four lessons expanding the manuscript's group-ring, cyclotomic-local-ring and alternating-character-product argument and its even Barker consequence, with independent review described as incomplete. [AI-generated per source] [family-level]
• Gradient Damage, Circulant Hadamard Conjecture, Cycle–Clique Ramsey Numbers and 7 More in Combinatorics (video compilation, 2026-10-15). The chapter beginning at 0:21 introduces circulant matrices and states this family's claimed Hadamard and Barker classifications, describing the animations as illustrations rather than proofs. [family-level]