Asymptotically optimal approximate Hadamard matrices
Boris Alexeev, John Jasper, Dustin G. Mixon
math.CO
Nov 18, 2025 · v2
math.FA
TL;DR
A key lemma (Lemma 3, on block-matrix orthogonalization) was auto-formalized in Lean via Harmonic's Aristotle; the Lean code is an arXiv ancillary file.
Abstract
An approximate Hadamard matrix is a well-conditioned square matrix with all entries in $\{\pm1\}$. We measure the quality of a matrix by its condition number, i.e., the ratio of its largest and smallest singular values. We prove that for any fixed positive $α<17/92$, every sufficiently large dimension admits an approximate Hadamard matrix with condition number at most $1+n^{-α}$. In particular, the smallest possible condition number tends to $1$ as $n\to\infty$. Conversely, there exists an absolute constant $c>0$ such that for every sufficiently large $n\not\equiv0\pmod4$, every $n\times n$ matrix with entries in $\{\pm1\}$ has condition number at least $1+c(\log n)/n$. Along the way, we resolve a problem of Jaming and Matolcsi concerning flat orthogonal matrices, and we conclude by describing several explicit infinite families of approximate Hadamard matrices.
Problem
Approximate Hadamard matrices are ±1 square matrices with condition number close to 1. The question is whether the smallest achievable condition number κ(n) tends to 1 as n grows, and how fast. A related open question of Jaming and Matolcsi asks whether flat orthogonal matrices exist in every large dimension.
Approach
Known Hadamard matrices are converted into flat orthogonal matrices by submatrix orthogonalization. These are then randomly rounded to ±1 matrices, and the matrix Bernstein inequality together with Weyl's inequality bounds the resulting condition number. A Ramsey-theory argument on the Gram matrix gives the lower bound. A supporting lemma on block-matrix orthogonalization, suggested by ChatGPT, was formalized in Lean using Aristotle.
Results
For any α<17/92, κ(n) ≤ 1+n^{-α} for all large n; under the Hadamard conjecture, α can be taken close to 1/4. In the other direction, κ(n) ≥ 1+c log n/n for large n not divisible by 4. The work also resolves the Jaming–Matolcsi problem and gives explicit families of approximate Hadamard matrices.
