exists_williamson_arrays_odd

Open

by jackjburleson · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

For every odd integer $k \geq 3$ , if there exist four $k \times k$ symmetric $\pm 1$ matrices $A, B, C, D$ that pairwise commute and satisfy $A^2 + B^2 + C^2 + D^2 = 4k I_k$ , then a Hadamard matrix of order $4k$ exists. This is the Williamson array existence conjecture at odd composite orders — one of the key remaining open cases in approaches to the general Hadamard conjecture.

Preamble

import Mathlib.LinearAlgebra.Matrix.Kronecker
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open Matrix

Formal statement

theorem exists_williamson_arrays_odd (k : ℕ) (hk_odd : Odd k) (hk_ge3 : 3 ≤ k) :
    ∃ A B C D : Matrix (Fin k) (Fin k) ℝ,
      (∀ i j, A i j = 1 ∨ A i j = -1) ∧
      (∀ i j, B i j = 1 ∨ B i j = -1) ∧
      (∀ i j, C i j = 1 ∨ C i j = -1) ∧
      (∀ i j, D i j = 1 ∨ D i j = -1) ∧
      A.transpose = A ∧ B.transpose = B ∧ C.transpose = C ∧ D.transpose = D ∧
      A * B = B * A ∧ A * C = C * A ∧ A * D = D * A ∧
      B * C = C * B ∧ B * D = D * B ∧ C * D = D * C ∧
      A * A + B * B + C * C + D * D = ((4 * k : ℕ) : ℝ) • (1 : Matrix (Fin k) (Fin k) ℝ) := by sorry

View graph