Hadamard's conjecture

References:

• Wikipedia
• Résolution d'une question relative aux déterminants by Jacques Hadamard, Bull. des sciences math., p.245, 1893

def IsHadamard {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop

A square matrix $M$ with $±1$-entries that satisfies the equality $|M| ≤ n^\frac{n}{2}$ is called a Hadamard matrix.

Equations

• IsHadamard M = ((∀ (i j : Fin n), M i j ∈ {1, -1}) ∧ |M.det| = ↑n ^ (↑n / 2))

def IsHadamard' {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop

Equivalently, a square matrix $M$ with $±1$-entries $|A| ≤ n^\frac{n}{2}.$ if it satisfies the equality $M^TM = n \cdot 1$, where $1$ denotes the unit matrix.

Equations

• IsHadamard' M = ((∀ (i j : Fin n), M i j ∈ {1, -1}) ∧ M.transpose * M = ↑n)

theorem HadamardConjecture (k : ℕ) : ∃ (M : Matrix (Fin (4 * k)) (Fin (4 * k)) ℝ), IsHadamard M

There exists a Hadamard matrix for all $n = 4k$.

def H12 : Matrix (Fin 12) (Fin 12) ℝ

Hadamard constructs a 12 x 12 matrix ...

Equations

• One or more equations did not get rendered due to their size.

theorem HadamardConjecture.variant : ∃ (M : Matrix (Fin (4 * 167)) (Fin (4 * 167)) ℝ), IsHadamard M

The smallest order for which no Hadamard matrix is presently known is $668 = 4 * 167$.