FormalConjectures.Wikipedia.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:

Wikipedia

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


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.

TOOD(firsching): complete and golf the proof

@[category test, AMS 15]
theorem declaration uses 'sorry'isHadamard_equiv_isHadamard' (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : IsHadamard' M ↔ IsHadamard M := byn:ℕM:Matrix (Fin n) (Fin n) ℝ⊢ IsHadamard' M ↔ IsHadamard M
  simp [IsHadamard, IsHadamard']n:ℕM:Matrix (Fin n) (Fin n) ℝ⊢ (∀ (i j : Fin n), M i j = 1 ∨ M i j = -1) → (M.transpose * M = ↑n ↔ |M.det| = ↑n ^ (↑n / 2))
  intro hn:ℕM:Matrix (Fin n) (Fin n) ℝh:∀ (i j : Fin n), M i j = 1 ∨ M i j = -1⊢ M.transpose * M = ↑n ↔ |M.det| = ↑n ^ (↑n / 2)
  let N := M.transpose * Mn:ℕ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.transpose * M = ↑n ↔ |M.det| = ↑n ^ (↑n / 2)
  constructormpn:ℕ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.transpose * M = ↑n → |M.det| = ↑n ^ (↑n / 2)mprn:ℕ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
  ·mpn:ℕ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.transpose * M = ↑n → |M.det| = ↑n ^ (↑n / 2) intro hmpn:ℕ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 = ↑n⊢ |M.det| = ↑n ^ (↑n / 2)
    have h_det : (M.transpose * M).det = n^((n : ℝ)) := byn:ℕM:Matrix (Fin n) (Fin n) ℝ⊢ IsHadamard' M ↔ IsHadamard M
      have : Matrix.diagonal (fun x : Fin n => (n : ℝ)) = (n : Matrix (Fin n) (Fin n) ℝ) := byn:ℕM:Matrix (Fin n) (Fin n) ℝ⊢ IsHadamard' M ↔ IsHadamard M
        rflAll goals completed! 🐙
      rw [h, ← this]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 = ↑nthis:(Matrix.diagonal fun x => ↑n) = ↑n := Eq.refl (Matrix.diagonal fun x => ↑n)⊢ (Matrix.diagonal fun x => ↑n).det = ↑n ^ ↑n
      norm_numAll goals completed! 🐙
    simp only [Matrix.det_mul, Matrix.det_transpose] at h_detmpn:ℕ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 ^ ↑n⊢ |M.det| = ↑n ^ (↑n / 2)
    rw [← Real.sqrt_mul_self_eq_abs M.det, h_det]mpn:ℕ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 ^ ↑n⊢ √(↑n ^ ↑n) = ↑n ^ (↑n / 2)
    have : √(↑n ^ (n : ℝ)) = (↑n ^ (n : ℝ)) ^ ((1 : ℝ)/2) := byn:ℕM:Matrix (Fin n) (Fin n) ℝ⊢ IsHadamard' M ↔ IsHadamard M
      rw [Real.rpow_div_two_eq_sqrt]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 ^ ↑n⊢ √(↑n ^ ↑n) = √(↑n ^ ↑n) ^ 1hxn:ℕ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 ^ ↑n⊢ 0 ≤ ↑n ^ ↑n
      ·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 ^ ↑n⊢ √(↑n ^ ↑n) = √(↑n ^ ↑n) ^ 1 simp only [Real.rpow_natCast, Real.rpow_one]All goals completed! 🐙
      ·hxn:ℕ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 ^ ↑n⊢ 0 ≤ ↑n ^ ↑n simp only [Real.rpow_natCast, Nat.cast_nonneg, pow_nonneg]All goals completed! 🐙
    rw [this]mpn:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ (↑n ^ ↑n) ^ (1 / 2) = ↑n ^ (↑n / 2)
    simpmpn:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ (↑n ^ n) ^ 2⁻¹ = ↑n ^ (↑n / 2)
    refine ((fun {x y z} hx hy hz ↦ (Real.eq_rpow_inv hx hy hz).mpr) ?_ ?_ ?_ ?_).symmmp.refine_1n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 0 ≤ ↑n ^ (↑n / 2)mp.refine_2n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 0 ≤ ↑n ^ nmp.refine_3n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 2 ≠ 0mp.refine_4n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ (↑n ^ (↑n / 2)) ^ 2 = ↑n ^ n
    ·mp.refine_1n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 0 ≤ ↑n ^ (↑n / 2) exact Real.rpow_nonneg (Nat.cast_nonneg' n) _All goals completed! 🐙
    ·mp.refine_2n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 0 ≤ ↑n ^ n simp only [Nat.cast_nonneg, pow_nonneg]All goals completed! 🐙
    ·mp.refine_3n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ 2 ≠ 0 norm_numAll goals completed! 🐙
    ·mp.refine_4n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ (↑n ^ (↑n / 2)) ^ 2 = ↑n ^ n rw [← Real.rpow_mul <| Nat.cast_nonneg' n]mp.refine_4n:ℕ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) := 
  Eq.mpr
    (id
      (congrArg (fun _a => √(↑n ^ ↑n) = _a)
        (Real.rpow_div_two_eq_sqrt 1
          (of_eq_true
            (Eq.trans (congrArg (LE.le 0) (Real.rpow_natCast (↑n) n))
              (isHadamard_equiv_isHadamard'._simp_4 (of_eq_true (isHadamard_equiv_isHadamard'._simp_3 n)) n))))))
    (of_eq_true
      (Eq.trans
        (congr (congrArg (fun x => Eq √x) (Real.rpow_natCast (↑n) n))
          (Eq.trans (congrArg (fun x => √x ^ 1) (Real.rpow_natCast (↑n) n)) (Real.rpow_one √(↑n ^ n))))
        (eq_self √(↑n ^ n))))⊢ ↑n ^ (↑n / 2 * 2) = ↑n ^ n
      norm_numAll goals completed! 🐙
  ·mprn:ℕ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 sorryAll goals completed! 🐙

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

@[category research open, AMS 15]
theorem declaration uses 'sorry'HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M := byk:ℕ⊢ ∃ M, IsHadamard M
  sorryAll goals completed! 🐙


@[category test, AMS 15]
theorem exists_hadamard_zero : ∃ M, IsHadamard (n := 0) M := by⊢ ∃ M, IsHadamard M
  use 0h⊢ IsHadamard 0
  simp [IsHadamard]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 satisifies the condition.

@[category test, AMS 15]
theorem declaration uses 'sorry'isHadamard_H12 : IsHadamard H12 := by⊢ IsHadamard H12
  sorryAll 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 declaration uses 'sorry'HadamardConjecture.variants.first_cases (k : ℕ) (h : k ≤ 166) :
    ∃ M, IsHadamard (n := 4 * k) M := byk:ℕh:k ≤ 166⊢ ∃ M, IsHadamard M
  sorryAll goals completed! 🐙

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

@[category research open, AMS 15]
theorem declaration uses 'sorry'HadamardConjecture.variants.«167» : ∃ M, IsHadamard (n := 4 * 167) M := by⊢ ∃ M, IsHadamard M
  sorryAll goals completed! 🐙


end Hadamard