Exactly three mutually unbiased bases in dimension six

2 papersLean

Proves \(N(6)=3\), resolving Zauner's dimension-six mutually unbiased bases conjecture: three such bases exist in ℂ⁶, but four cannot. The exclusion is a complete certified computation under the stated binary64 arithmetic and compiler conditions. An independent companion proves the Matolcsi–Ruzsa–Weiner Fourier-vanishing conjecture for order-six complex Hadamard matrices outside Tao's cubic equivalence class.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

The maximum number of mutually unbiased bases in dimension six

OpenAI · September 24, 2026

We prove that the maximum number of mutually unbiased orthonormal bases in ℂ⁶ is three, resolving Zauner's dimension-six MUB conjecture. The upper bound is computer-assisted: under the stated binary64 arithmetic and compiler conditions, a complete execution of the documented verification pipeline excludes four arbitrary complex bases.

Read PDF Download Source

Cite

@misc{OAI:The-maximum-number-of-mutually-unbiased-bases-in-dimension-six-September-24-2026,
  author = {{OpenAI}},
  title = {{The maximum number of mutually unbiased bases in dimension six}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-maximum-number-of-mutually-unbiased-bases-in-dimension-six-September-24-2026/The-maximum-number-of-mutually-unbiased-bases-in-dimension-six-September-24-2026.pdf}{OAI:The-maximum-number-of-mutually-unbiased-bases-in-dimension-six-September-24-2026}},
  year = {2026}
}

Exact Fourier certificates for complex Hadamard matrices of order six

OpenAI · September 24, 2026

We prove the Fourier-vanishing conjecture of Matolcsi, Ruzsa, and Weiner: every complex Hadamard matrix of order six outside Tao's cubic equivalence class has a vanishing character sum at every permutation of \((1,1,1,-1,-1,-1)\). We also give an exact certificate excluding seven mutually unbiased bases in ℂ⁶; by Weiner's completion theorem, this yields an upper bound of five. Both certificates use only integer and rational arithmetic, and the complete verifier is included.

Read PDF Download Source

Cite

@misc{OAI:Exact-Fourier-certificates-for-complex-Hadamard-matrices-of-order-six-September-24-2026,
  author = {{OpenAI}},
  title = {{Exact Fourier certificates for complex Hadamard matrices of order six}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Exact-Fourier-certificates-for-complex-Hadamard-matrices-of-order-six-September-24-2026/Exact-Fourier-certificates-for-complex-Hadamard-matrices-of-order-six-September-24-2026.pdf}{OAI:Exact-Fourier-certificates-for-complex-Hadamard-matrices-of-order-six-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The paper claims that at most three mutually unbiased orthonormal bases exist in \(\mathbb C^6\). The linked formalization proves a weaker family bound: every family in its mutually unbiased bases model has at most five members. It also proves a Fourier character-sum vanishing statement for order-six complex Hadamard matrices not equivalent to the Tao matrix, uniformly over coordinate permutations.

The selected statement does not establish the paper's upper bound of three or its computer-assisted exclusion of four arbitrary bases.

The linked formalization proves a cancellation lemma used in the order-six complex Hadamard analysis. Let \(H\) and its entrywise square both be complex Hadamard matrices, and fix two distinct rows. If the cubes of their six entrywise ratios take only two distinct values, then the sum of the row-ratio terms over either specified cube fiber is zero.

This is a supporting Fourier cancellation statement. The paper's full character-sum vanishing theorem and its mutually unbiased bases bound are outside this selected statement.

Comparator links

Result	Comparator statement
Order-six Hadamard Fourier vanishing and a five-basis upper bound	MUBSix.lean
Cube-fiber cancellation for order-six Hadamard row ratios	HadamardCubeFiber.lean

Scope note on GitHub →