Formal target: Corpus.WikipediaHadamard.HadamardConjecture

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.

Exact formal statement

∀ (k : Nat), Exists.{1} fun M => Corpus.WikipediaHadamard.IsHadamard M

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record