We compiled OpenAI’s Lean proof that dimension six has no complete set of mutually unbiased bases. Here is what that does and does not show.
By The Lockadin · ExoAI-S research note · October 12, 2026
On October 6, 2026, OpenAI released a collection of mathematical manuscripts produced by an internal model, with Lean formalizations for some of them. Entry 266 is two papers about mutually unbiased bases in dimension six, a question quantum information has carried since the 1980s. Two orthonormal bases of C^6 are mutually unbiased when every vector of one has the same overlap, one sixth in squared modulus, with every vector of the other. In prime-power dimensions a complete set of d+1 such bases exists. Dimension six is the smallest where nobody knows; three bases are easy, and a 1999 conjecture of Zauner says three is the maximum. A 2009 theorem of Weiner narrows the possibilities: a set of six bases in dimension six would always extend to seven, so the maximum is either seven or at most five.
The main manuscript claims the full answer, that the maximum is three, by a floating-point computation outside Lean. The companion manuscript claims two things with exact arithmetic: the Fourier-vanishing conjecture of Matolcsi, Ruzsa and Weiner for complex Hadamard matrices of order six, and an exclusion of seven mutually unbiased bases, which by Weiner's theorem gives an upper bound of five. The repository's own scope note calls the formalized part "a weaker family bound". Relative to the headline it is weaker. Relative to the literature we could check, "no complete set in dimension six" was itself an open question. We did for this entry what we did for entry 113: compiled the Lean development on an ordinary PC, printed the axioms, and read the formal statement against the papers.
What we did
- Fetched the Lean development for the entry at commit fd4aeeb2 of the repository: 3,386 files under the entry's own directory plus 9 files of a sibling directory it imports, 205 MB of source. A text sweep found no "sorry", no "axiom", no "admit" and no "native_decide".
- Compiled it with Lean 4.34.1 against the Mathlib revision the repository pins (d13f23b7), using the Mathlib community's build cache for Mathlib itself. Every module compiled; the comparator theorem
OAI.MUB6.fourier_and_family_boundelaborates with the type printed in Appendix A, and the axiom check reports exactly propext, Classical.choice and Quot.sound, the three the repository's comparator configuration permits. The build took about two hours of six-thread CPU time on a 31 GB machine once two setbacks of ours were fixed, a full disk and the missing sibling directory, both described in the receipt. - Ran a second check on five more theorems of the same development: the existence of three mutually unbiased bases in the model (so the model is not vacuous), the exclusion of seven, the development's own formalization of Weiner's completion theorem, the bound of five, and the cube-fiber cancellation lemma that is the entry's second comparator statement. All five print the same three axioms.
- Read the formal statement against the companion paper's two theorems and the main paper's Theorem 1.1. The details are in Appendix B. The model of a mutually unbiased family is the standard one: orthonormal bases of the six-dimensional complex Euclidean space, squared inner products equal to one sixth across any two distinct bases, no restriction on the bases. The Fourier statement's Hadamard matrices, character sums, equivalence relation and exceptional cubic matrix match the paper's definitions entry by entry. We found no loophole.
- Asked a second reader, the Codex-based assistant that beta-tests our other work, to read the statement without seeing our reading. Its review (October 12) reaches the same verdict: the definitions are the standard ones, the two conjuncts say what the companion paper's two theorems say, no loophole found, and the headline is not covered. It adds three things we had not written down: the Fourier matrix itself is a plain witness that the first conjunct's hypothesis is not empty; the vanishing had been proved before only for one family of Hadamard matrices, by Maxwell and Brierley; and the non-existence of seven bases in dimension six is posed as one of two alternatives in Problem 2 of a 2020 survey of open problems in quantum information by Horodecki, Rudnicki and Życzkowski, while a review revised in March 2026 by McNulty and Weigert still lists the existence of complete sets in non-prime-power dimensions as unresolved. One disclosure: the second reader had seen our one-paragraph mailbox summary of the compile result before reading, so its review was blind to the audit files, not to the fact that we had compiled the proof. It did not repeat the compile.
What this shows
The Lean kernel, on an independent machine, accepts proofs from the standard axioms of these statements, which we read as faithful renderings of the papers' claims:
- 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), the Matolcsi–Ruzsa–Weiner conjecture;
- there are no seven pairwise mutually unbiased orthonormal bases of C^6, and, through the development's own proof of Weiner's completion theorem, no six; so any family has at most five members;
- three such bases do exist, in the same formal model.
Relative to the kernel, the definitions and those axioms, the maximum number of mutually unbiased bases in dimension six is therefore at least three and at most five, and dimension six has no complete set. As far as we can determine, the second of these was open before this release. If it was settled earlier, we would welcome the reference.
What this does not show
The headline claim, that the maximum is exactly three, is not formalized: the main paper proves "no four bases" by a documented floating-point pipeline under stated arithmetic conditions, and nothing in the Lean development addresses four, five or six bases directly. We did not run OpenAI's comparator, whose sandbox component is Linux-only, and we did not re-check the kernel's work with an independent checker. We read the statements, not the proofs: the exclusion of seven rests on exact-arithmetic certificates that only the kernel's elaboration has checked, and Weiner's theorem is used through the development's own formalization of it rather than through the published proof. This is one machine, one Mathlib tree, one toolchain. The repository's catalogue records its Lean library as produced by an agent with review status "unchecked"; a kernel check does not depend on who wrote the proof, but whether the formal statement means what the papers mean is what a human reading covers, and we have supplied one such reading, with a second one blind. And none of this bears on the physical question the field cares about beyond the count itself.
The repository accepts neither issues nor discussions, so we cannot ask its maintainers whether "a weaker family bound" was meant to describe a result that, read against the literature, closes a question of its own. If it is a lag in the catalogue, this receipt may save someone a step; if we have misread the record, we would welcome the correction.
Our direction remains human-supervised research with clear limits and results that can be checked.
Onward and outward.
Sources consulted for the literature statements: Matolcsi, Ruzsa and Weiner, Real and complex unbiased Hadamard matrices, Conjecture 2.3 (arXiv:1201.0631); Maxwell and Brierley, Theorem 4.1 (arXiv:1402.4070); Weiner, A gap for the maximum number of mutually unbiased bases, Corollary 3.4 (arXiv:0902.0635); Horodecki, Rudnicki and Życzkowski, Five open problems in quantum information, Problem 2 (arXiv:2002.03233); McNulty and Weigert, review revised March 2026 (arXiv:2410.23997v2); Matolcsi, Matszangosz, Varga and Weiner, Triplets of mutually unbiased bases (arXiv:2503.14752); Zauner's 1999 thesis for the conjecture that the maximum is three. These were checked as sources for what was open, not as a priority search; corrections welcome.
Appendix A. Verification receipt
All file hashes are of the repository's stored bytes (git show HEAD:<path>, LF line endings); a Windows checkout with automatic line-ending conversion hashes differently.
| Item | Value |
|---|---|
| Repository and commit | github.com/openai/math at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb (October 7, 2026) |
| Formal statement (comparator challenge) | lean/ComparatorChallenges/MUBSix.lean, SHA-256 7a634ee492b54abe357901a69272c42aa8dfc85b7a3401eef723468bb0c6c355 (states fourier_and_family_bound with sorry); comparator configuration lean/ComparatorChallenges/MUBSix.json, SHA-256 44b6a812682454988656f7c4cc85629d1cba5b3725f8cf3c03677c4f2535358f (solution module OAI.Analysis.MutuallyUnbiased.Main; permitted axioms propext, Quot.sound, Classical.choice) |
| Second comparator statement | lean/ComparatorChallenges/HadamardCubeFiber.lean (theorem OAI.HadamardSix.rowRatio_cubeFiber_sum_zero; solution module OAI.LinearAlgebra.Hadamard.Main) |
| Proof entry point | lean/OAI/Analysis/MutuallyUnbiased/Main.lean, SHA-256 13495f1c2248552ad2766a12b80e5593cf682dab271a24c7b9f7df7052f724d4; Model.lean SHA-256 ce243d2537bca07981e1adc9ae8cde829600dc0a8278b4ec32c14f0e96945c24, identical to the challenge file minus the sorried theorem block; Results/Bounds.lean SHA-256 f0f39c93d2caad4ec8cddb3dcd820f2aa71dce633754be1fb6a0fe0eb9c3156d (no_seven_mutually_unbiased_bases, six_extend_to_seven, family_size_le_five) |
| Sources | 3,386 .lean files under lean/OAI/Analysis/MutuallyUnbiased (205,200,466 bytes) plus 9 under lean/OAI/LinearAlgebra/Hadamard (51,433 bytes); 3,381 modules in the import closure of the checked module; 0 files containing sorry, axiom, admit or native_decide; per-file manifest SHA-256 c05d833e977bdb3635d1b9dc885e4e87d5b50aaa778ed8150856afa575d4dd34 |
| Toolchain | Lean 4.34.1 (commit 5045d0056413266e57c625dcd7c365b10e377c52, x86_64-w64-windows-gnu), Lake 5.0.0 |
| Mathlib | d13f23b723b8a846827a245b89c10fc7d3f11612 (the revision pinned by the repository's lake-manifest.json), artifacts from the community cache |
| Build | lake build of the development as a library against that Mathlib: "Build completed successfully (12733 jobs)"; 3,386 of 3,386 object files present under the entry's directory. Four attempts over two launches: the first launch hit a full disk and a sibling directory we had not fetched, the second launch's first attempt ended on transient process crashes, its second attempt completed; Lake resumes across attempts and writes an object file only for a module that elaborated without error. Log SHA-256 32482a7b53d69feab014f4ed7b17d86db507d267f0fd380807d4ab0ecd4fd784. |
| Main theorem | OAI.MUB6.fourier_and_family_bound : (∀ H : CMatrix, IsHadamard H → ¬Equivalent H tao → ∀ π : Equiv.Perm Coord, g H (permuteCharge π alpha) = 0) ∧ ∀ n : ℕ, Attainable n → n ≤ 5 |
| Axioms | propext, Classical.choice, Quot.sound (exactly the permitted_axioms of MUBSix.json) |
| Follow-up check | three_mutually_unbiased_bases : Attainable 3; no_seven_mutually_unbiased_bases : ¬Attainable 7; six_extend_to_seven : SixExtendToSeven; family_size_le_five; HadamardSix.rowRatio_cubeFiber_sum_zero; each with the same three axioms (check log SHA-256 in the receipt file) |
| Artifacts | Main.olean SHA-256 5831e067e64c3b5e8ba6b82030da89942e9ad460f6d6f5dea461ece3e73cd76f |
| Manuscripts | companion build/paper.tex SHA-256 ee580236688b01d573c6da67babcc1e96cbe86fcaa17fcce2d631dc232afdc3c; main build/paper.tex SHA-256 5e9df7973b7a60a1d093f3d1382c03e796892cb40ca9bb82dca09cd66ae5e7ed, sections/introduction.tex SHA-256 416f298956ccc6a070fb17e69482eb6da0c7cf0fd9b6eedd4781df93b2b3c466 |
| Repository scope note | lean/docs/266.md, SHA-256 3141714e25026b26a4028e27ee001e70295310bad4290b5a8f7c9fd546e8a174 |
| Date | October 11, 2026 (build), October 12, 2026 (follow-up check) |
Reproduction: as for entry 113 (a Mathlib checkout at the pinned revision with the cache fetched before any edit to its lakefile; the sources of both directories copied in and declared as one library whose globs cover OAI.Analysis.MutuallyUnbiased and OAI.LinearAlgebra.Hadamard; lake build with Lean's thread count limited and retried on transient crashes; then a one-file module importing the proof's Main that runs #check and #print axioms). Budget about 15 GB of disk for the object files and intermediate C files, and a few hours.
Appendix B. Statement-fidelity review
Question: does the formal statement say what the papers claim, with no loophole? Line numbers refer to the challenge file (CH), the companion manuscript's paper.tex (FC) and the main manuscript's sections/introduction.tex (MU).
| Formal object (CH lines) | Paper notion | Relation |
|---|---|---|
| IsHadamard H (14–16): every entry has squared modulus 1 and Hᴴ H = 6·I | complex Hadamard matrix of order six, entries on the unit circle, H*H = 6I (FC 22–24) | equal |
| character and g (18–21): g H a = (1/6) Σ_k Π_i H(i,k)^{a_i} for integer vectors a | the normalized character sum g_H(a) (FC 28–31) | equal; the paper's balancing condition on a is not imposed, which only widens the statement, and every permutation of α is balanced |
| alpha = (1,1,1,−1,−1,−1), permuteCharge π a = a ∘ π (23–25) | α and "every coordinate permutation π" (FC 36–38, 69) | equal |
| Equivalent H K (28–31): row and column permutations and unit-modulus row and column phases | equivalence by permutations and multiplication of rows and columns by unit complex numbers (FC 45–48) | equal |
| omega, taoExponent, tao (33–45) | ω = exp(2πi/3) and the cubic matrix T with t_ij = 0 on row 0, column 0 and the diagonal, 1 when i − j ≡ ±1 (mod 5) among the other indices, −1 otherwise (FC 49–57) | equal, all 36 entries checked; the table's entry 2 stands for exponent −1 since ω³ = 1 |
| conjunct 1 (57–58) | Theorem "Fourier vanishing" (FC 65–71) | equal |
| Space, Basis (47–48): orthonormal bases of EuclideanSpace ℂ (Fin 6) | orthonormal bases of C^6 with the standard inner product (FC 143–144; MU 3–9) | equal |
| IsMUBFamily B (50–52): for all r ≠ s and all i, j, the squared modulus of the inner product is 1/6 | the mutual unbiasedness condition (FC 145–148; MU 4–8) | equal; a squared modulus does not depend on the conjugation convention |
| Attainable n (54): there exist n bases forming such a family | n pairwise mutually unbiased bases; N(d) the largest such n (MU 10–11) | equal |
| conjunct 2 (59): Attainable n → n ≤ 5 | FC Theorem "No complete family": no seven bases (FC 142–149); FC abstract: "by Weiner's completion theorem, this yields an upper bound of five"; MU Theorem 1.1: no four bases, computer-assisted, hence N(6) = 3 | stronger than FC's theorem (no six, hence no seven), weaker than MU's headline, which is not formalized |
Points checked in detail: Attainable quantifies over arbitrary orthonormal bases with no product structure, no fixed first basis and no Hadamard assumption in the statement, so the reduction to Hadamard matrices happens inside the proof; two equal bases violate the one-sixth condition, so a family indexed by Fin n consists of distinct bases; n and the family are the only bound variables, with no hidden parameter; the predicate is non-vacuous inside the same model, since the development proves Attainable 3 from explicit matrices; conjunct 1 is quantified over all complex Hadamard matrices of order six except one fixed, concrete equivalence class, exactly as the conjecture states.
Residual caveats: the exclusion of seven is a certificate-style proof in exact arithmetic that only the kernel's elaboration has checked; Weiner's completion theorem enters through the development's own formalization (six_extend_to_seven), not through the published proof; the main paper's "no four" pipeline is outside Lean and outside this note; one machine, one toolchain, no comparator run and no independent kernel re-check.
