1. FormalConjectures
  2. Wikipedia
  3. Hadamard
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Hadamard's conjecture

References:

namespace Hadamard

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

def IsHadamard {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop := (∀ (i j : Fin n), M i j ∈ ({1, -1} : Finset ℝ)) ∧ |M.det| = n ^ ((n : ℝ) / 2)

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.

def IsHadamard' {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop := (∀ (i j : Fin n), M i j ∈ ({1, -1} : Finset ℝ)) ∧ M.transpose * M = ↑n

Both definitions are equivalent.

TODO(firsching): complete and golf the proof

n:ℕM:Matrix (Fin n) (Fin n) ℝh✝:∀ (i j : Fin n), M i j = 1 ∨ M i j = -1N:Matrix (Fin n) (Fin n) ℝ := M.transpose * Mh:M.transpose * M = ↑nh_det:M.det * M.det = ↑n ^ ↑nthis:√(↑n ^ ↑n) = (↑n ^ ↑n) ^ (1 / 2)⊢ ↑n ^ (↑n / 2 * 2) = ↑n ^ n All goals completed! 🐙 n:ℕM:Matrix (Fin n) (Fin n) ℝh:∀ (i j : Fin n), M i j = 1 ∨ M i j = -1N:Matrix (Fin n) (Fin n) ℝ := M.transpose * M⊢ |M.det| = ↑n ^ (↑n / 2) → M.transpose * M = ↑n All goals completed! 🐙

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

@[category research open, AMS 15] theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M := k:ℕ⊢ ∃ M, IsHadamard M All goals completed! 🐙@[category test, AMS 15] theorem exists_hadamard_zero : ∃ M, IsHadamard (n := 0) M := ⊢ ∃ M, IsHadamard M ⊢ IsHadamard 0 All goals completed! 🐙

Hadamard constructs a 12 x 12 matrix ...

def H12 : Matrix (Fin 12) (Fin 12) ℝ := !![ 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1; 1, 1, 1, -1, -1, -1, -1, -1, -1, 1, 1, 1; 1, 1, 1, -1, -1, -1, 1, 1, 1, -1, -1, -1; 1, -1, -1, 1, -1, -1, -1, 1, 1, -1, 1, 1; 1, -1, -1, -1, 1, -1, 1, -1, 1, 1, -1, 1; 1, -1, -1, -1, -1, 1, 1, 1, -1, 1, 1, -1; 1, -1, 1, -1, 1, 1, -1, 1, -1, -1, -1, 1; 1, -1, 1, 1, -1, 1, -1, -1, 1, 1, -1, -1; 1, -1, 1, 1, 1, -1, 1, -1, -1, -1, 1, -1; 1, 1, -1, -1, 1, 1, -1, -1, 1, -1, 1, -1; 1, 1, -1, 1, -1, 1, 1, -1, -1, -1, -1, 1; 1, 1, -1, 1, 1, -1, -1, 1, -1, 1, -1, -1 ]

which satisfies the condition.

@[category test, AMS 15] theorem isHadamard_H12 : IsHadamard H12 := ⊢ IsHadamard H12 All goals completed! 🐙

For all $k ≤ 166$, it is known there that there is a Hadamard matrix of size $4 * k$.

@[category research solved, AMS 15] theorem HadamardConjecture.variants.first_cases (k : ℕ) (h : k ≤ 166) : ∃ M, IsHadamard (n := 4 * k) M := k:ℕh:k ≤ 166⊢ ∃ M, IsHadamard M All goals completed! 🐙

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

@[category research open, AMS 15] theorem HadamardConjecture.variants.«167» : ∃ M, IsHadamard (n := 4 * 167) M := ⊢ ∃ M, IsHadamard M All goals completed! 🐙end Hadamard