Williamson Conjecture

### What is the conjecture

For every positive integer $m$, there exist four pairwise commuting symmetric circulant matrices $A, B, C, D$ with entries in $\{-1, +1\}$ of order $m$ such that $A^2 + B^2 + C^2 + D^2 = 4mI_m$, where $I_m$ is the $m \times m$ identity matrix. These matrices are called **Williamson matrices**.

The conjecture was formulated to provide a construction route for Hadamard matrices, which are $n \times n$ matrices with entries in $\{-1, +1\}$ satisfying $HH^T = H^T H = nI_n$. When Williamson matrices exist for order $m$, they can be arranged into a Williamson array to construct Hadamard matrices of order $4m$.

**Status**: The conjecture has been shown to be false. In 1993, Dragomir Ž. Ðoković found via exhaustive computer search that Williamson matrices do not exist for all orders, with order 35 being a known counterexample.

**Sources:**
- https://en.wikipedia.org/wiki/Williamson_conjecture, https://encyclopediaofmath.org/wiki/Williamson_matrices, https://uwaterloo.ca/mathcheck/new-matrices/williamson-conjecture-counterexample, https://projecteuclid.org/journals/journal-of-the-mathematical-society-of-japan/volume-37/issue-4/Williamson-Hadamard-matrices-and-Gauss-sums/10.2969/jmsj/03740703.pdf

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-01-20)

Mathlib has basic matrix definitions and linear algebra infrastructure (Matrix type, identity matrix, transpose, matrix multiplication). However, formalizing Williamson matrices requires: (1) defining circulant matrices as a specific matrix construction, (2) specifying the commutativity constraint for pairs of matrices, (3) defining the specific polynomial equation $A^2 + B^2 + C^2 + D^2 = 4mI_m$, and (4) potentially encoding known counterexamples like order 35. The core matrix operations exist, but the specialized combinatorial structure of Williamson matrices needs to be built on top of existing matrix theory.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-15

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.

No repository files, tests, or entry points are identified in the issue. Start by reviewing the existing matrix definitions and formalized conjecture declarations, then determine how circulant matrices, commutativity, and the Williamson identity fit the repository's current infrastructure. Done means adding a checked Lean statement of the conjecture with the required definitions and references.

Written by the indexing model from the issue text.