Zauner's conjecture: at most three mutually unbiased bases in dimension six
Orthonormal bases of are mutually unbiased if for all , . Let be the largest number of pairwise unbiased bases. Always , with equality in prime-power dimensions (Ivanovic; Wootters-Fields), so is the first open case. Three bases exist in from a tensor-product construction; numerical searches (Butterley-Hall, Brierley-Weigert) and restricted exclusions (Grassl; Jaming et al. for the Fourier family) found no fourth. Zauner conjectured in his 1991 diploma thesis that three is the maximum; Klappenecker and Rotteler state as Conjecture 1. Is ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Mutually unbiased bases; complex Hadamard matrices
- Posed by
- Gerhard Zauner (diploma thesis, Vienna, 1991); stated as Conjecture 1 by Klappenecker and Rotteler (2004)
- Year posed
- 1991
- Years open
- 35y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Unreviewed
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 45 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1 (computer-assisted): there are no four pairwise mutually unbiased orthonormal bases in , hence , the lower bound coming from the explicit tensor-product triple. The proof covers every second basis (an arbitrary complex Hadamard matrix) by certified phase balls and excludes two further bases in each by a clique search with rounding margins. It is conditional on the stated binary64 arithmetic and on the complete execution it documents. The companion paper gives an exact rational certificate only for , and that weaker bound is what the release's Lean formalization proves.
What the AI did
The release README says every result in openai/math was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not one of the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The upper bound is a computer-assisted exhaustive cover of all complex Hadamard matrices of order six, certified under stated binary64 arithmetic and compiler conditions; the manuscript says it rests on a fresh complete execution and that a separate September 7 execution reported in its source manuscript was not authenticated.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against Zauner's conjecture; it states that under the arithmetic and compiler conditions of its appendix, a documented complete execution excludes four pairwise unbiased bases, so . The conclusion is conditional on that computation. The manuscript points to an accompanying verification archive (verification/computation/README.md, verification/REPRODUCE.md, verification/code/proof_run.py); fetching those paths from the manuscript folder at the pinned commit returned 404, and the folder's README has no verification section, so the computation was not re-run here. Lean: lean/docs/266.md says the linked formalization (MUBSix) proves only that every family has at most five members, plus the companion's Fourier vanishing; it does not establish the bound of three, so this entry is Unreviewed, not Lean-checked.
Sources
- PaperCompanion: Exact Fourier certificates for complex Hadamard matrices of order six (N(6) <= 5)
- Lean proofLean (five-basis bound only): OAI.MUB6.fourier_and_family_boundLean scope note for this family (lean/docs/266.md)
- CodeOpenAI math release: The maximum number of mutually unbiased bases in dimension six