OP-00076 Lean verified: disproved

Counting real Hadamard matrices

For $n \ge 1$ let $H(n)$ be the number of Hadamard matrices of order $n$, that is, of matrices $A \in \{-1, 1\}^{n \times n}$ with $AA^{\mathsf T} = nI_n$. Matrices are counted individually, with their row and column labels, so two that differ by permuting or negating rows or columns are counted separately. If one Hadamard matrix of order $n$ exists, permuting its rows gives $H(n) \ge n!$. Ferber, Jain and Zhao proved $H(n) \le 2^{(1 - c)n^2/2}$ for an absolute constant $c > 0$ and every sufficiently large multiple $n$ of $4$.

Problem. Is there an absolute constant $C > 0$ such that $$H(n) \le 2^{C n \log_2 n}$$ for every positive integer $n$ divisible by four?

Source: Ferber, Jain and Zhao (2022), Conjecture 1.3, stated there as H(n) = 2^{O(n log n)} for n = 4m.

Imported from github.com/ajt60gaibb/OpenProblemsInNLA.

Classification

Primary: CO — Combinatorics
Secondary: PR
Keywords: Hadamard matrices, OpenProblemsInNLA, sign matrices

References

@article{ferber2022,
  author        = {Ferber, Asaf and Jain, Vishesh and Zhao, Yufei},
  title         = {On the number of {H}adamard matrices via anti-concentration},
  journal       = {Combin. Probab. Comput.},
  volume        = {31},
  number        = {3},
  year          = {2022},
  pages         = {455--477},
  doi           = {10.1017/S0963548321000377},
  eprint        = {1808.07222},
  archivePrefix = {arXiv},
}
@misc{openproblemsinnla-fr12,
  author       = {Townsend, Alex},
  title        = {{FR-12}: Counting real Hadamard matrices},
  howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
  year         = {2026},
  url          = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/frames-and-matrix-designs/FR-12/README.md},
  note         = {Read at commit e375a6f, 2026-09-30},
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00076.

namespace RegistryProblems.OP_00076
noncomputable section

open scoped BigOperators

abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ

/-- Exactly the canonical labeled real sign matrices and one-sided Gram identity.
There is no quotient by row/column permutations or signs. -/
def IsRealHadamard {n : ℕ} (A : Mat n) : Prop :=
  (∀ i j, A i j = 1 ∨ A i j = -1) ∧
    A * A.transpose = (n : ℝ) • (1 : Mat n)

/-- Individual matrices, with their original row and column labels. -/
def HadamardMatrices (n : ℕ) := {A : Mat n // IsRealHadamard A}

/-- The exact finite count. Finiteness of the displayed matrix subtype is a
required theorem, so `Nat.card` is not used to hide an infinite set. -/
def hadamardCount (n : ℕ) : ℕ := Nat.card (HadamardMatrices n)

/-- OP-00076: Counting real Hadamard matrices -/
def _root_.RegistryProblems.Problem_OP_00076 : Prop :=
  ∃ C : ℝ, 0 < C ∧ ∀ n : ℕ, 1 ≤ n → 4 ∣ n →
    (hadamardCount n : ℝ) ≤
      (2 : ℝ) ^ (C * (n : ℝ) * (Real.log (n : ℝ) / Real.log 2))

end
end RegistryProblems.OP_00076

Formalised by George Stepaniants (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_00076

theorem resolution : RegistryProblems.Problem_OP_00076 := by
  sorry

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

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

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

theorem disproof : ¬ RegistryProblems.Problem_OP_00076 := 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.

Resolution claims

FR-12: a labeled Hadamard counting counterexample v1 GitHub ↗

George Stepaniants

Proves a complete negative answer to the original labeled real Hadamard counting conjecture. A genuine finite matrix subtype and an injective restricted doubling construction give m! H(m)^2 ≤ H(2m), the exact source power-of-two lower bound, and a counterexample for every positive real constant.

Disproof · verified · canonical statement matched · posted on GitHub 12 Sep 2026

A matching-indexed doubling counterexample v1 GitHub ↗

George Stepaniants

Let $H(n)$ count labeled real Hadamard matrices of order $n$. An injective construction gives $H(2m)\ge(2m-1)!!\,H(m)^2$: given a perfect matching of the $2m$ row positions and Hadamard matrices $A,B$ of order $m$, the two rows of the $i$th pair are $(A_{i,\cdot},B_{i,\cdot})$ and $(A_{i,\cdot},-B_{i,\cdot})$, and the matching, $A$ and $B$ are recovered from the output, so no assumption about automorphism groups or …

Disproof · not verified · fidelity not established · posted on GitHub 12 Sep 2026

Status history

When	Change	By	Reason
2026-10-05	Needs verification → Lean verified	—	Verified here: OpenProblemsInNLA @ e375a6f, FR-12/lean/.

Citing this problem

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

OP-00076, "Counting real Hadamard matrices", clopen.solutions.