Wikipedia · research open · AMS 15
unsolvedsorry — nobody on it
Hadamard's conjecture
Conjecture · HadamardConjecture
There exists a Hadamard matrix for all .
Formal statement · Lean 4.lean
theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M := by
sorryProof. sorry
Nobody has tried yet.