clopen.solutions
Subjects › CO
OP-00032 Open

The Hadamard conjecture

Submit a result

A Hadamard matrix of order $n$ is an $n \times n$ matrix with entries $\pm1$ whose columns are pairwise orthogonal. Sylvester's construction gives one of every order $2^k$.

Problem. Prove or disprove that there is a Hadamard matrix of order $n$ for every positive multiple $n$ of $4$.

Source: Named after Hadamard (1893), who asked for which orders such matrices exist; also attributed to Paley (1933). Conjecture 14 of Randomstrasse101, in Bandeira's “Did just a couple of deviations suffice all along?” (2024); Entry 6 of arXiv:2504.20539.

Imported from github.com/MColbrook/AIM.

The statement is adapted from randomstrasse101.math.ethz.ch, whose text is available under CC BY 4.0.

Classification

Primary
CO — Combinatorics
Secondary
RA
Keywords
combinatorial designs, Hadamard matrices, Randomstrasse101
Literature checked
Oct. 2, 2026 by clemens-admin

References

@misc{randomstrasse2024,
  author = {Bandeira, Afonso S. and Kireeva, Anastasia and Maillard, Antoine and R{\"o}dder, Almut},
  title = {{Randomstrasse101}: Open Problems of 2024},
  year = {2025},
  eprint = {2504.20539},
  archivePrefix = {arXiv}
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00032. 

/-- OP-00032: The Hadamard conjecture -/
def Problem_OP_00032 : Prop :=
  ∀ (k : ℕ), ∃ M : Matrix (Fin (4 * k)) (Fin (4 * k)) ℝ,
  (∀ (i j : Fin (4 * k)), M i j ∈ ({1, -1} : Finset ℝ)) ∧
    |M.det| = ((4 * k : ℕ) : ℝ) ^ (((4 * k : ℕ) : ℝ) / 2)

Formalised by The Formal Conjectures Authors (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"

In your proof:

import RegistryProblems.OP_00032

theorem resolution : RegistryProblems.Problem_OP_00032 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it: 

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00032"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one: 

theorem disproof : ¬ RegistryProblems.Problem_OP_00032 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn. 

OP-00032, "The Hadamard conjecture", clopen.solutions.