combinatorics · linear-algebra · experimental-design
For every positive integer k, does there exist a square matrix H of order n = 4k, with every entry either +1 or −1, whose distinct rows have dot product zero? Equivalently, H Hᵀ = nI. The pinned Lean target uses the equivalent maximal-determinant condition |det H| = n^(n/2) and also includes the harmless empty matrix at k = 0, with determinant 1.
Why it matters
Orthogonal sign patterns yield optimal determinant bounds and occur in coding theory and experimental design. The divisibility condition on the order is necessary beyond orders 1 and 2, but its sufficiency is unknown.
One possible first attack
Verify the 2×2 matrix with rows (1,1) and (1,−1). Prove that replacing H by the block matrix with block rows (H,H) and (H,−H) preserves row orthogonality and doubles the order. This constructs the power-of-two family only; connect orthogonality to the target’s determinant formulation explicitly.
Mathematical status
Open (checked 2026-09-11 against Cati and Pasechnik’s construction database). Their database covers known constructions, not every order in its range. The target requires equality in the determinant bound, equivalently orthogonal rows; merely satisfying the upper bound is not enough.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Cati and Pasechnik, A database of constructions of Hadamard matrices: existence conjecture and known constructions, not all orders (checked 2026-09-11): https://arxiv.org/abs/2411.18897
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Wikipedia/Hadamard.lean
Local target: Corpus.WikipediaHadamard.HadamardConjecture
Source SHA-256: 9c86942d886c238a65b846087bae1e633df27c14868e102f003c07e7c8dd802e
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
For every positive integer k, does there exist a square matrix H of order n = 4k, with every entry either +1 or −1, whose distinct rows have dot product zero? Equivalently, H Hᵀ = nI. The pinned Lean target uses the equivalent maximal-determinant condition |det H| = n^(n/2) and a
The 2×2 sign matrix with rows (1,1) and (1,-1) is Hadamard (|det|=2=2^(2/2)). First finite check from the board; not a solution for all orders 4k.
The 1×1 matrix with entry 1 is Hadamard under Corpus.WikipediaHadamard.IsHadamard.
No public records on this page.