Hadamard.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 4 contain sorry, 0 declared as axioms

Hadamard's conjecture

References:

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

Imports (1)

FormalConjecturesUtil

Imported by 2 files

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

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Real
Proof uses: And, Membership.mem, Finset, Insert.insert, OfNat.ofNat, Singleton.singleton, Neg.neg, Eq, abs, Matrix.det, HPow.hPow, HDiv.hDiv
22 instances, coercions and auxiliary constants left out.
```
def IsHadamard {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop :=
…
```
def Hadamard.IsHadamard' 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 line 43 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Matrix, Fin, Real
Proof uses: And, Membership.mem, Finset, Insert.insert, OfNat.ofNat, Singleton.singleton, Neg.neg, Eq, HMul.hMul, Matrix.transpose
17 instances, coercions and auxiliary constants left out.
```
def IsHadamard' {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Prop :=
…
```
theorem Hadamard.isHadamard_equiv_isHadamard' Both definitions are equivalent sorry line 53 source
Source documentation
Both definitions are equivalent.
TODO(firsching): complete and golf the proof

depends on sorry what this means
Statement uses: Nat, Matrix, Fin, Real, Iff, Hadamard.IsHadamard', Hadamard.IsHadamard
Proof uses: Eq.mpr, Or, Eq, OfNat.ofNat, Neg.neg, HMul.hMul, Matrix.transpose, abs, Matrix.det, HPow.hPow, HDiv.hDiv, id, Eq.trans, And, congr, congrArg, congrFun', Membership.mem, Finset, Insert.insert and 49 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
```
theorem isHadamard_equiv_isHadamard' (n : ℕ) (M : Matrix (Fin n) (Fin n) ℝ) : IsHadamard' M ↔ IsHadamard M := by
…
```
Mentions: Hadamard.IsHadamard', Hadamard.IsHadamard
theorem Hadamard.HadamardConjecture There exists a Hadamard matrix for all $n = 4k$ sorry line 90 source
Source documentation
There exists a Hadamard matrix for all $n = 4k$.

depends on sorry what this means
Statement uses: Nat, Exists, Matrix, Fin, HMul.hMul, OfNat.ofNat, Real, Hadamard.IsHadamard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadamardConjecture (k : ℕ) : ∃ M, IsHadamard (n := 4 * k) M := by
…
```
Mentions: Hadamard.IsHadamard
theorem Hadamard.exists_hadamard_zero line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Matrix, Fin, OfNat.ofNat, Nat, Real, Hadamard.IsHadamard
Proof uses: Exists.intro, of_eq_true, And, Membership.mem, Finset, Insert.insert, Singleton.singleton, Neg.neg, Eq, abs, Matrix.det, HPow.hPow, HDiv.hDiv, Eq.trans, True, congr, congrArg, forall_congr, False, Or and 10 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Hadamard.H12 Hadamard constructs a 12 x 12 matrix line 101 source
Source documentation
Hadamard constructs a 12 x 12 matrix ...

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Matrix, Fin, OfNat.ofNat, Nat, Real
Proof uses: Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Neg.neg
8 instances, coercions and auxiliary constants left out.
```
def H12 : Matrix (Fin 12) (Fin 12) ℝ :=
…
```
theorem Hadamard.isHadamard_H12 which satisfies the condition line 118 source
Source documentation
which satisfies the condition.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Hadamard.IsHadamard, OfNat.ofNat, Nat, Hadamard.H12
Proof uses: Eq, Matrix, Fin, Real, HMul.hMul, Matrix.transpose, HSMul.hSMul, Eq.mpr, id, congrArg, Eq.symm, propext, Matrix.ext_iff, of_eq_true, Eq.trans, And, HAdd.hAdd, Matrix.vecCons, Matrix.vecEmpty, Neg.neg and 110 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem isHadamard_H12 : IsHadamard H12 := by
…
```
Mentions: Hadamard.IsHadamard, Hadamard.H12
theorem Hadamard.HadamardConjecture.variants.first_cases For all $k ≤ 166$, it is known there that there is a Hadamard matrix of size $4 * k$ sorry line 132 source
Source documentation
For all $k ≤ 166$, it is known there that there is a Hadamard matrix of size $4 * k$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Matrix, Fin, HMul.hMul, Real, Hadamard.IsHadamard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadamardConjecture.variants.first_cases (k : ℕ) (h : k ≤ 166) :
    ∃ M, IsHadamard (n := 4 * k) M := by
…
```
Mentions: Hadamard.IsHadamard
theorem Hadamard.HadamardConjecture.variants.«167» The smallest order for which no Hadamard matrix is presently known is $668 = 4 * 167$ sorry line 140 source
Source documentation
The smallest order for which no Hadamard matrix is presently known is $668 = 4 * 167$.

depends on sorry what this means
Statement uses: Exists, Matrix, Fin, HMul.hMul, Nat, OfNat.ofNat, Real, Hadamard.IsHadamard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadamardConjecture.variants.«167» : ∃ M, IsHadamard (n := 4 * 167) M := by
…
```
Mentions: Hadamard.IsHadamard