Existence of Hadamard matrices at specified orders

For which multiples of four can explicit Hadamard matrices be constructed? The recorded targets are orders 2884,4532,7004,7172,7828,8476,9476 and 11948, using Cooper–Wallis constructions from periodic T-matrices and Williamson quadruples.

Why it matters and what counts as progress

Why it matters: Explicit constructions fill existence parameters while also clarifying which printed ingredient recipes are actually available.

What counts as progress: Construct and exactly verify matrices at unrecorded orders, or prove a genuine obstruction to a specified ingredient rather than to all constructions at that order.

How the problem developed

1933 · Construction family [1]
Raymond E. A. C. Paley Gave infinite construction families and conjectured that a Hadamard matrix exists at every positive order divisible by four.
August 2026 · Reported constructions [2]
Levent Alpöge, Philippe Voinov and Saul Reynolds-Haertle, with Claude assistance Announced constructions for the twelve previously unknown orders below 2000, including order 668.
30 Aug 2026 · Formalized constructions [3]
JD-Jones-ASES; Claude Fable 5 contributed to the formalization Released Lean formalizations establishing Hadamard existence at eight orders from 2884 through 11948 that the cited construction database did not record as known.
19 Oct 2026 · Verification and new constructions [2]
Ronan Egan, Ilias S. Kotsireas, Stephen London and Pádraig Ó Catháin Verified the twelve August constructions and reported sixteen further orders with constructions, while listing 95 orders up to 10000 still unresolved in the published literature.

AI contribution

AI-assisted Hadamard constructions cover eight orders

Using periodic T-matrix quadruples of orders 103 and 163 and symmetric-circulant Williamson quadruples of orders 7, 11, 13, 17, 19, 23 and 29, a formalized Cooper–Wallis construction gives Hadamard matrices at orders 2884, 4532, 7004, 7172, 7828, 8476, 9476 and 11948. A separate parity result rules out Miyamoto’s displayed C2-matrix ingredient at positive block orders not congruent to 1 mod 4.

AI involvementAI-centered

ImportanceNotable

Technical verificationFormal (Lean 4/Mathlib kernel with finite decide checks, transitive axiom audit and Comparator statement matching)

Human understandingFew