Open quantum problems

The 3 problem files in FormalConjectures/OpenQuantumProblems that state a research or textbook statement, at commit 2055e5ad, one article each.

Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.

TheoremOpen Quantum Problem 13: Mutually unbiased bases#

Mathematical problem

For each integer \(d \ge 2\), determine the maximum number \(k\) for which there exist orthonormal bases \(\mathcal{B}_1, \dots, \mathcal{B}_k\) of the complex Hilbert space \(\mathbb{C}^d\) such that any two distinct bases are mutually unbiased.

Concretely, if \(\mathcal{B}_r = \{ e_0^{(r)}, \dots, e_{d-1}^{(r)} \}\) and \(\mathcal{B}_s = \{ e_0^{(s)}, \dots, e_{d-1}^{(s)} \}\), then \(\mathcal{B}_r\) and \(\mathcal{B}_s\) are mutually unbiased if for all \(i, j\) and all \(r \ne s\), \(|\langle e_i^{(r)}, e_j^{(s)} \rangle| = d^{-1/2}\).

The problem is therefore to determine the maximal value \(\mu(d) := \max \{ k : \text{there exist } k \text{ pairwise mutually unbiased orthonormal bases in } \mathbb{C}^d \}\).

In this file, an orthonormal basis is represented by a unitary matrix whose columns are the basis vectors. For two such bases U and V, the matrix relativeUnitary U V, which is \(U^\dagger V\), contains all cross-basis overlaps as its entries. Since Lean works more smoothly with squared norms, we formalize mutual unbiasedness by requiring \(\| (relativeUnitary\ U\ V)_{ij} \|^2 = 1 / d\) for all \(i, j\), which is equivalent to \(|\langle e_i^{(r)}, e_j^{(s)} \rangle| = d^{-1/2}\).

Background

Mutually unbiased bases are a basic structure in finite-dimensional quantum theory. They arise in quantum state determination, quantum tomography, quantum cryptography, finite geometry, and combinatorics.

A general upper bound is \(\mu(d) \le d + 1\). Equality is known when \(d\) is a prime power, via constructions over finite fields. For composite dimensions that are not prime powers, the exact value of \(\mu(d)\) is in general open.

The smallest and most famous unresolved case is \(d = 6\). The IQOQI OQP page emphasizes this dimension in particular: although many equivalent reformulations are known, no construction yielding more than three mutually unbiased bases in dimension six is known.

What this file formalizes

This file is organized around the quantity IsMaxMUBCount d k, which expresses that \(k\) is the maximum number of mutually unbiased orthonormal bases in dimension \(d\).

• the open theorem mutuallyUnbiasedBases expresses the full problem for all \(d \ge 2\);
• the open theorem mutuallyUnbiasedBases_dim6 expresses the especially important case \(d = 6\);
• the solved theorem mutuallyUnbiasedBases_dim2 proves the qubit case \(\mu(2) = 3\);
• the solved theorems mutuallyUnbiasedBases_dim6_bounds and mutuallyUnbiasedBases_dim6_bounds.variants.upper_five record the bounds \(3 \le \mu(6) \le 7\) and \(\mu(6) \le 5\).

References

Primary source list entry: - IQOQI Vienna Open Quantum Problems, problem 13: https://oqp.iqoqi.oeaw.ac.at/mutually-unbiased-bases - Master list of open quantum problems: https://oqp.iqoqi.oeaw.ac.at/open-quantum-problems

Foundational papers

• I. D. Ivanović, Geometrical description of quantal state determination, J. Phys. A 14, 3241-3245 (1981).
• W. K. Wootters and B. D. Fields, Optimal state-determination by mutually unbiased measurements, Ann. Phys. 191, 363-381 (1989).

General constructions and surveys

• A. Klappenecker and M. Rötteler, Constructions of mutually unbiased bases, in Finite Fields and Applications, LNCS 2948 (2004).

Dimension six and the maximal-number problem

• M. Grassl, On SIC-POVMs and MUBs in Dimension 6, arXiv:quant-ph/0406175 (2004).
• P. Butterley and W. Hall, Numerical evidence for the maximum number of mutually unbiased bases in dimension six, Phys. Lett. A 369, 5-8 (2007), arXiv:quant-ph/0701122.
• S. Brierley and S. Weigert, Maximal Sets of Mutually Unbiased Quantum States in Dimension Six, Phys. Rev. A 78, 042312 (2008), arXiv:0808.1614.
• P. Raynal, X. Lü, and B.-G. Englert, Mutually unbiased bases in dimension six: The four most distant bases, Phys. Rev. A 83, 062303 (2011), arXiv:1103.1025.
• [OAI26a] OpenAI, Exact Fourier certificates for complex Hadamard matrices of order six. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/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
• [OAI26b] OpenAI, The maximum number of mutually unbiased bases in dimension six. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/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

Remark on the status of \(d = 6\)

The dimension-six case is not known to be solved. At present, the best-known general picture is: - \(3 \le \mu(6) \le 5\), where the upper bound was proved by an internal OpenAI model in September 2026 [OAI26a] with a formal Lean proof, - a companion preprint [OAI26b] claims \(\mu(6) = 3\) by a computer-assisted argument that is not formalised, - and several analytic and numerical works give strong evidence that one cannot go beyond \(3\).

This is why the theorem mutuallyUnbiasedBases_dim6 is marked as an open research statement.

Quoted from FormalConjectures/OpenQuantumProblems/13.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 9 research or textbook statements: 6 open and 3 solved. It also has 2 test statements and 28 API statements, counted here but not shown.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim2

Proved here.

In dimension \(2\), the maximum number of mutually unbiased orthonormal bases is \(3\).

theorem mutuallyUnbiasedBases_dim2 : IsMaxMUBCount 2 3

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 526.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds

Solved: stated here; a Lean proof is at https://github.com/XC0R/formal-conjectures/blob/c8733543568e8011288a9fa7ef33375f5e5907d3/FormalConjectures/OpenQuantumProblems/13.lean#L1168.

Known general bounds in dimension \(6\): the maximal number of mutually unbiased bases satisfies \(3 \le \mu(6) \le 7\).

theorem mutuallyUnbiasedBases_dim6_bounds :
    HasMUBs 6 3 ∧ ∀ m : ℕ, HasMUBs 6 m → m ≤ 7

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 534.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds.variants.upper_five

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/MutuallyUnbiased/Main.lean#L22.

The upper bound \(\mu(6) \le 5\): every family of mutually unbiased bases in \(\mathbb{C}^6\) has at most five members. This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof. That proof represents each basis as an OrthonormalBasis of EuclideanSpace ℂ (Fin 6), which corresponds to the columns of a unitary matrix here.

theorem mutuallyUnbiasedBases_dim6_bounds.variants.upper_five :
    ∀ m : ℕ, HasMUBs 6 m → m ≤ 5

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 545.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim6

Open: stated without proof.

Special case in dimension \(6\): determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^6\).

theorem mutuallyUnbiasedBases_dim6 :
    IsMaxMUBCount 6 (mutuallyUnbiasedBases_dim6.answer)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 556.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim10

Open: stated without proof.

Special case in dimension \(10\) (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^{10}\).

theorem mutuallyUnbiasedBases_dim10 :
    IsMaxMUBCount 10 (mutuallyUnbiasedBases_dim10.answer)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 565.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim12

Open: stated without proof.

Special case in dimension \(12\) (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^{12}\).

theorem mutuallyUnbiasedBases_dim12 :
    IsMaxMUBCount 12 (mutuallyUnbiasedBases_dim12.answer)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 574.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim14

Open: stated without proof.

Special case in dimension \(14\) (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^{14}\).

theorem mutuallyUnbiasedBases_dim14 :
    IsMaxMUBCount 14 (mutuallyUnbiasedBases_dim14.answer)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 583.

OpenQuantumProblem13.mutuallyUnbiasedBases_dim15

Open: stated without proof.

Special case in dimension \(15\) (not a prime power): determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^{15}\).

theorem mutuallyUnbiasedBases_dim15 :
    IsMaxMUBCount 15 (mutuallyUnbiasedBases_dim15.answer)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 592.

OpenQuantumProblem13.mutuallyUnbiasedBases

Open: stated without proof.

Open Quantum Problem 13: determine the maximal number of mutually unbiased orthonormal bases in \(\mathbb{C}^d\) for \(d \ge 2\).

theorem mutuallyUnbiasedBases (d : ℕ) (hd : 2 ≤ d) :
    IsMaxMUBCount d (mutuallyUnbiasedBases.answer d)

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/13.lean, line 601.

Sources

• FormalConjectures/OpenQuantumProblems/13.lean at 2055e5ad
• https://oqp.iqoqi.oeaw.ac.at/mutually-unbiased-bases

LeanOpenQuantumProblem13.mutuallyUnbiasedBases_dim2 · OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds · OpenQuantumProblem13.mutuallyUnbiasedBases_dim6_bounds.variants.upper_five · OpenQuantumProblem13.mutuallyUnbiasedBases_dim6 · OpenQuantumProblem13.mutuallyUnbiasedBases_dim10 · OpenQuantumProblem13.mutuallyUnbiasedBases_dim12 · OpenQuantumProblem13.mutuallyUnbiasedBases_dim14 · OpenQuantumProblem13.mutuallyUnbiasedBases_dim15 · OpenQuantumProblem13.mutuallyUnbiasedBases

TheoremOpen Quantum Problem 23: SIC-POVMs#

Mathematical problem

The OQP page presents three increasingly strong formulations of this problem. In this file we formalize the first one, closest to the physics terminology: existence of a symmetric informationally complete POVM in every finite dimension.

A SIC-POVM in dimension \(d\) can be represented by a family of \(d^2\) normalized vectors in \(\mathbb{C}^d\) whose pairwise squared overlaps are all equal to \((d + 1)^{-1}\). We encode such a family as a map Fin (d ^ 2) → StateVector d.

Background

SIC-POVMs are a basic structure in finite-dimensional quantum information. They are closely related to equiangular lines, tight frames, quantum state reconstruction, and finite-dimensional measurement theory. The open problem asks whether such families exist in every dimension.

What this file formalizes

This file formalizes the existence problem for symmetric informationally complete POVMs through the predicate HasSICPOVM d.

More precisely, it contains the following layers.

Core API

The main definitions formalized in this file are: - StateVector d: a state vector in ℂ^d; - mkStateVector: constructor from coordinates in the computational basis; - IsNormalized ψ: normalization predicate for a state vector; - overlapSq φ ψ: squared magnitude of the inner-product overlap; - HasConstantOverlapSq c Φ: constant pairwise squared-overlap condition; - sicOverlapSq d: the SIC overlap value (d + 1)⁻¹; - IsSICFamily d Φ: the predicate that a family of d^2 vectors in ℂ^d is a SIC family; - HasSICPOVM d: existence of a SIC family in dimension d.

In addition, the file includes explicit witness families and convenient constructors used in the low-dimensional benchmark cases: - vec2, vec3; - qubitSICFamily; - hesseFamily; - bb84Family.

Complete open conjecture

The main open theorem is: - sicPOVMs, expressing the conjecture that for every d ≥ 1, there exists a SIC-POVM in dimension d.

Special cases

The file also isolates several special cases: - solved low-dimensional benchmark cases: hasSICPOVM_zero, hasSICPOVM_one, hasSICPOVM_two, hasSICPOVM_three; - a negative benchmark result: bb84Family_not_isSICFamily, showing that the BB84 family in dimension 2 does not form a SIC family; - selected open benchmark dimensions: hasSICPOVM_56, hasSICPOVM_58, hasSICPOVM_59, hasSICPOVM_60, hasSICPOVM_64, hasSICPOVM_68, hasSICPOVM_69, hasSICPOVM_70, hasSICPOVM_71, hasSICPOVM_72, hasSICPOVM_75.

Test lemmas

The file includes the following test lemmas and benchmark-support statements: - hasConstantOverlapSq_singleton; - sicOverlapSq_one, sicOverlapSq_two, sicOverlapSq_three, sicOverlapSq_pos; - isSICFamily_singleton_iff, isSICFamily_one_of_normalized; - qubitSICFamily_normalized, qubitSICFamily_pairwise; - hesseFamily_normalized, hesseFamily_pairwise; - bb84Family_normalized.

At present, these @[category test, AMS 15 47 81] results are included with placeholder proofs by sorry; they are intended to be proved in the next PR.

References

Primary source list entry: - IQOQI Vienna Open Quantum Problems, problem 23: https://oqp.iqoqi.oeaw.ac.at/sic-povms-and-zauners-conjecture - Formal Conjectures issue #1823: https://github.com/google-deepmind/formal-conjectures/issues/1823

Foundational references

• J. M. Renes, R. Blume-Kohout, A. J. Scott, and M. C. Caves, Symmetric informationally complete quantum measurements, J. Math. Phys. 45, 2171-2180 (2004), arXiv:quant-ph/0310075.
• G. Zauner, Quantum Designs: Foundations of a Noncommutative Design Theory, PhD thesis, University of Vienna (1999).

Quoted from FormalConjectures/OpenQuantumProblems/23.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 12 research or textbook statements: 12 open. It also has 17 test statements, counted here but not shown.

OpenQuantumProblem23.hasSICPOVM_56

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(56\).

theorem hasSICPOVM_56 : HasSICPOVM 56

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 320.

OpenQuantumProblem23.hasSICPOVM_58

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(58\).

theorem hasSICPOVM_58 : HasSICPOVM 58

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 324.

OpenQuantumProblem23.hasSICPOVM_59

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(59\).

theorem hasSICPOVM_59 : HasSICPOVM 59

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 328.

OpenQuantumProblem23.hasSICPOVM_60

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(60\).

theorem hasSICPOVM_60 : HasSICPOVM 60

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 332.

OpenQuantumProblem23.hasSICPOVM_64

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(64\).

theorem hasSICPOVM_64 : HasSICPOVM 64

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 336.

OpenQuantumProblem23.hasSICPOVM_68

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(68\).

theorem hasSICPOVM_68 : HasSICPOVM 68

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 340.

OpenQuantumProblem23.hasSICPOVM_69

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(69\).

theorem hasSICPOVM_69 : HasSICPOVM 69

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 344.

OpenQuantumProblem23.hasSICPOVM_70

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(70\).

theorem hasSICPOVM_70 : HasSICPOVM 70

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 348.

OpenQuantumProblem23.hasSICPOVM_71

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(71\).

theorem hasSICPOVM_71 : HasSICPOVM 71

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 352.

OpenQuantumProblem23.hasSICPOVM_72

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(72\).

theorem hasSICPOVM_72 : HasSICPOVM 72

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 356.

OpenQuantumProblem23.hasSICPOVM_75

Open: stated without proof.

Benchmark open subproblem: existence of a SIC-POVM in dimension \(75\).

theorem hasSICPOVM_75 : HasSICPOVM 75

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 360.

OpenQuantumProblem23.sicPOVMs

Open: stated without proof.

Do SIC-POVMs exist in every finite dimension?

theorem sicPOVMs :
    ∀ d : ℕ, 1 ≤ d → HasSICPOVM d

Category research open; AMS 15 Linear and multilinear algebra; matrix theory, 47 Operator theory, 81 Quantum theory. Declared in FormalConjectures/OpenQuantumProblems/23.lean, line 366.

Sources

• FormalConjectures/OpenQuantumProblems/23.lean at 2055e5ad
• https://oqp.iqoqi.oeaw.ac.at/sic-povms-and-zauners-conjecture

LeanOpenQuantumProblem23.hasSICPOVM_56 · OpenQuantumProblem23.hasSICPOVM_58 · OpenQuantumProblem23.hasSICPOVM_59 · OpenQuantumProblem23.hasSICPOVM_60 · OpenQuantumProblem23.hasSICPOVM_64 · OpenQuantumProblem23.hasSICPOVM_68 · OpenQuantumProblem23.hasSICPOVM_69 · OpenQuantumProblem23.hasSICPOVM_70 · OpenQuantumProblem23.hasSICPOVM_71 · OpenQuantumProblem23.hasSICPOVM_72 · OpenQuantumProblem23.hasSICPOVM_75 · OpenQuantumProblem23.sicPOVMs

TheoremOpen Quantum Problem 35: existence of absolutely maximally entangled pure states#

Problem: For which numbers of parties \(n\) and local dimensions \(d\) does there exist a pure absolutely maximally entangled state \(\psi\)?

A pure state \(\psi\) on \(n\) parties of local dimension \(d\) is called absolutely maximally entangled (AME) if, for every subset of at most half of the parties, the corresponding reduced density matrix is maximally mixed.

References: - Open Quantum Problems, Problem 35: https://oqp.iqoqi.oeaw.ac.at/existence-of-absolutely-maximally-entangled-pure-states - Formal Conjectures issue #3452: https://github.com/google-deepmind/formal-conjectures/issues/3452 - W. Helwig, W. Cui, A. Riera, J. I. Latorre, and H.-K. Lo, Absolute Maximal Entanglement and Quantum Secret Sharing, Phys. Rev. A 86, 052335 (2012), arXiv:1204.2289. - D. Goyeneche, D. Alsina, J. I. Latorre, A. Riera, and K. Życzkowski, Absolutely Maximally Entangled states, combinatorial designs and multi-unitary matrices, Phys. Rev. A 92, 032316 (2015), arXiv:1506.08857. - A. Higuchi and A. Sudbery, How entangled can two couples get?, Phys. Lett. A 273, 213-217 (2000), arXiv:quant-ph/0005013. - A. J. Scott, Multipartite entanglement, quantum-error-correcting codes, and entangling power of quantum evolutions, Phys. Rev. A 69, 052330 (2004), arXiv:quant-ph/0310137. - F. Huber, O. Gühne, and J. Siewert, Absolutely maximally entangled states of seven qubits do not exist, Phys. Rev. Lett. 118, 200502 (2017), arXiv:1608.06228. - F. Huber and M. Grassl, Quantum Codes of Maximal Distance and Highly Entangled Subspaces, Quantum 4, 284 (2020), arXiv:1907.07733. - S. A. Rather, A. Burchardt, W. Bruzda, G. Rajchel-Mieldzioć, A. Lakshminarayan, and K. Życzkowski, Thirty-six entangled officers of Euler: Quantum solution to a classically impossible problem, Phys. Rev. Lett. 128, 080507 (2022), arXiv:2104.05122. - G. Rajchel-Mieldzioć, R. Bistroń, A. Rico, A. Lakshminarayan, and K. Życzkowski, Absolutely maximally entangled pure states of multipartite quantum systems, arXiv:2508.04777 (2025). - S. Bevins and Y. Bidav, Symmetry-guided constructions of absolutely maximally entangled states in five open cases, arXiv:2608.05781 (2026). - F. Shi, X. Zhang, Q. Zhao, and L. Li, Complete Existence Classification of Seven-Partite Absolutely Maximally Entangled States, arXiv:2608.01011 (2026).

This file formalizes the problem of determining for which pairs \((n,d)\) there exists an absolutely maximally entangled pure state \(\mathrm{AME}(n,d)\).

We represent an \(n\)-partite state of local dimension \(d\) by the finite-dimensional Hilbert space EuclideanSpace ℂ (Config n d), whose coordinates in the computational basis are amplitudes. The helper mkStateVector turns an amplitude function into such a state, and normalization is imposed explicitly via IsNormalized, i.e. via the ambient \(L^2\) norm.

The main reusable lemma is reducedDensityFirst_of_completion: if a state is a uniform superposition over the graph of an injective completion function completion : Config m d → Config (n - m) d, then the reduced state on the first \(m\) parties is maximally mixed.

As demonstration, we show that the Bell states with \(n=2\) and GHZ states with \(n=3\) are AME states, and the GHZ state with \(n=4\) is not an AME state.

Quoted from FormalConjectures/OpenQuantumProblems/35.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 29 research or textbook statements: 10 open and 19 solved. It also has 6 test statements and 27 API statements, counted here but not shown.

OpenQuantumProblem35.ame_2_exists

Proved here.

The Bell state witnesses the existence of \(\mathrm{AME}(2,d)\) for every local dimension \(d \ge 2\).

theorem ame_2_exists {d : ℕ} (hd : 2 ≤ d) : ExistsAME 2 d

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 646.

OpenQuantumProblem35.ame_3_exists

Proved here.

The \(3\)-party GHZ state witnesses the existence of \(\mathrm{AME}(3,d)\) for every local dimension \(d \ge 2\).

theorem ame_3_exists {d : ℕ} (hd : 2 ≤ d) : ExistsAME 3 d

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 651.

OpenQuantumProblem35.ame_2_2_exists

Proved here.

Source-backed benchmark statement: the Bell state witnesses the existence of an \(\mathrm{AME}(2,2)\) state.

theorem ame_2_2_exists : ExistsAME 2 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 716.

OpenQuantumProblem35.ame_3_2_exists

Proved here.

Source-backed benchmark statement: the three-qubit GHZ state witnesses the existence of an \(\mathrm{AME}(3,2)\) state.

theorem ame_3_2_exists : ExistsAME 3 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 721.

OpenQuantumProblem35.ame_5_2_exists

Solved: stated here; a Lean proof is at https://github.com/zblore/fc-ame-5-2/blob/f0720e63065eb40c58a40f7b7af3d21f94d06453/AME52/FormalTarget.lean#L25-L26.

Source-backed benchmark statement: an \(\mathrm{AME}(5,2)\) state exists. This is one of the four qubit cases \(n=2,3,5,6\); see the OQP page and Scott (2004).

theorem ame_5_2_exists : ExistsAME 5 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 728.

OpenQuantumProblem35.ame_6_2_exists

Solved: stated here; a Lean proof is at https://github.com/zblore/fc-ame-6-2/blob/2a69b05aa65fec335b7e981deab2848865e9a688/AME62/FormalTarget.lean#L25-L26.

Source-backed benchmark statement: an \(\mathrm{AME}(6,2)\) state exists. This is one of the four qubit cases \(n=2,3,5,6\); see the OQP page and Scott (2004).

theorem ame_6_2_exists : ExistsAME 6 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 735.

OpenQuantumProblem35.ame_4_2_not_exists

Solved: stated here; a Lean proof is at https://github.com/zblore/fc-ame-4-2/blob/201550986844ea1e7fff36dc48681ca8b3c1600b/AME42/FormalTarget.lean#L26-L33.

Source-backed benchmark statement: no \(\mathrm{AME}(4,2)\) state exists; see Higuchi--Sudbery (2000) and the OQP page.

theorem ame_4_2_not_exists : ¬ ExistsAME 4 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 742.

OpenQuantumProblem35.ame_7_2_not_exists

Solved: stated here without proof.

Source-backed benchmark statement: no \(\mathrm{AME}(7,2)\) state exists; see Huber--Gühne--Siewert (2017) and the OQP page.

theorem ame_7_2_not_exists : ¬ ExistsAME 7 2

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 747.

OpenQuantumProblem35.ame_7_exists_iff

Solved: stated here without proof.

For a physical local dimension \(d \ge 2\), a seven-party AME state exists exactly when \(d \ge 3\). The hypothesis excludes the degenerate dimension \(d = 1\), for which the unique computational-basis state is AME under the definitions of this file. Shi--Zhang--Zhao--Li (2026) construct cyclic quadratic-phase states in every odd dimension and a coupled binary--odd-dimensional state in every dimension congruent to 2 modulo 4; together with power-of-two constructions and the product property, this covers every d ≥ 3.

theorem ame_7_exists_iff (d : ℕ) (hd : 2 ≤ d) : ExistsAME 7 d ↔ 3 ≤ d

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 757.

OpenQuantumProblem35.ame_4_3_exists

Solved: stated here; a Lean proof is at https://github.com/AllenGrahamHart/FormalConjectures-Bench/blob/8fb9479e9cbfde68d6990ed008b24c883cbd2750/formalizations/openquantum35_ame43/OpenQuantum35AME43Formalization.lean#L333.

Source-backed benchmark statement: an \(\mathrm{AME}(4,3)\) state exists; see Helwig et al. (2012) and Goyeneche et al. (2015).

theorem ame_4_3_exists : ExistsAME 4 3

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 764.

OpenQuantumProblem35.ame_4_6_exists

Solved: stated here; a Lean proof is at https://github.com/zblore/fc-ame-4-6/blob/d42273127096f5cbdc2c05f6d727f2dc75d5ea81/AME46/FormalTarget.lean#L23-L24.

Source-backed benchmark statement: an \(\mathrm{AME}(4,6)\) state exists; see Rather et al. (2022).

theorem ame_4_6_exists : ExistsAME 4 6

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 771.

OpenQuantumProblem35.ame_7_6_open

Proved here.

An \(\mathrm{AME}(7,6)\) state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026).

theorem ame_7_6_open :
    ExistsAME 7 6

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 779.

OpenQuantumProblem35.ame_7_10_open

Proved here.

An \(\mathrm{AME}(7,10)\) state exists, by the complete seven-party classification of Shi--Zhang--Zhao--Li (2026).

theorem ame_7_10_open :
    ExistsAME 7 10

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 786.

OpenQuantumProblem35.ame_8_4_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(8,4)\) state exist?

theorem ame_8_4_open :
    ExistsAME 8 4

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 792.

OpenQuantumProblem35.ame_8_6_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(8,6)\) state exist?

theorem ame_8_6_open :
    ExistsAME 8 6

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 798.

OpenQuantumProblem35.ame_8_10_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(8,10)\) state exist?

theorem ame_8_10_open :
    ExistsAME 8 10

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 804.

OpenQuantumProblem35.ame_9_6_open

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/ame-9-6-lean/blob/500ee827dffbeed9bb2ed502adcd6690943a7463/lean/AME96/FormalTarget.lean#L13.

Open benchmark statement: does an \(\mathrm{AME}(9,6)\) state exist?

Answer: Yes. A witness found by Kenta Kitamura (KitaKen1 on GitHub) is given here: https://github.com/KitaKen1/ame-9-6-lean

theorem ame_9_6_open :
    ExistsAME 9 6

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 817.

OpenQuantumProblem35.ame_9_10_open

Solved: stated here; a Lean proof is at https://github.com/niketp03/atlas-fc-verified/blob/15e4b3a7584e218cec531aeaf71cce72a8a9ecb1/AtlasFCSolutions/Oqp35.lean#L1238.

Open benchmark statement: does an \(\mathrm{AME}(9,10)\) state exist?

Solved: a Lean 4 proof, derived from the Atlas proofs in facebookresearch/atlas-lean, is linked in formal_proof.

theorem ame_9_10_open :
    ExistsAME 9 10

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 832.

OpenQuantumProblem35.ame_10_6_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(10,6)\) state exist?

theorem ame_10_6_open :
    ExistsAME 10 6

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 838.

OpenQuantumProblem35.ame_10_10_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(10,10)\) state exist?

theorem ame_10_10_open :
    ExistsAME 10 10

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 844.

OpenQuantumProblem35.ame_11_3_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(11,3)\) state exist?

theorem ame_11_3_open :
    ExistsAME 11 3

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 850.

OpenQuantumProblem35.ame_11_4_open

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/91bed229b434b68d66f5fd35cdcfee19a79985e8/FormalConjectures/OpenQuantumProblems/35.lean#L1861.

Open benchmark statement: does an \(\mathrm{AME}(11,4)\) state exist?

Answer: AME(11, 4) exists. The graph state defined by the circulant matrix Gamma over \(GF(4)\) with first row \((0, 0, 0, 1, ω, ω, ω, ω, 1, 0, 0)\) is an absolutely maximally entangled state of \(11\) ququarts. This result has been found by Moritz Firsching and Goran Žužić using an experimental pipeline

Before, it was already known that there is a quantum code for [11,0]]_5, which corresponds to an AME(11,4) state (which is another approach to a solution).

theorem ame_11_4_open :
    ExistsAME 11 4

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 868.

OpenQuantumProblem35.ame_11_5_open

Solved: stated here; a Lean proof is at https://github.com/google-deepmind/formal-conjectures/blob/47383bf7fbe86effc9ac184446e320f26ddbee3a/FormalConjectures/OpenQuantumProblems/35.lean#L2138.

Open benchmark statement: does an \(\mathrm{AME}(11,5)\) state exist?

The DeepMind prover agent has shown that such a state exists.

theorem ame_11_5_open :
    ExistsAME 11 5

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 879.

OpenQuantumProblem35.ame_11_6_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(11,6)\) state exist?

theorem ame_11_6_open :
    ExistsAME 11 6

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 885.

OpenQuantumProblem35.ame_11_10_open

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/ame-11-10-lean/blob/6b7d009a43970587a3386b690221bec4339ce271/lean/AME11_10FC.lean#L15-L21.

Open benchmark statement: does an \(\mathrm{AME}(11,10)\) state exist?

Answer: Yes. A witness found by Kenta Kitamura (KitaKen1 on GitHub) is given here: https://github.com/KitaKen1/ame-11-10-lean

theorem ame_11_10_open :
    ExistsAME 11 10

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 899.

OpenQuantumProblem35.ame_12_5_open

Solved: stated here without proof.

Does an \(\mathrm{AME}(12,5)\) state exist?

The answer is yes. Bevins and Bidav construct an explicit Hermitian self-dual MDS code with parameters \([12,6,7]_{25}\), whose associated nonbinary stabilizer state is an \(\mathrm{AME}(12,5)\) state.

theorem ame_12_5_open :
    ExistsAME 12 5

Category research solved; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 909.

OpenQuantumProblem35.ame_12_6_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(12,6)\) state exist?

theorem ame_12_6_open :
    ExistsAME 12 6

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 915.

OpenQuantumProblem35.ame_12_10_open

Open: stated without proof.

Open benchmark statement: does an \(\mathrm{AME}(12,10)\) state exist?

theorem ame_12_10_open :
    ExistsAME 12 10

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 921.

OpenQuantumProblem35.oqp_35

Open: stated without proof.

Open Quantum Problem 35: classify all pairs \((n,d)\) with \(n \ge 2\) and \(d \ge 2\) for which an \(\mathrm{AME}(n,d)\) state exists.

theorem oqp_35 :
    {nd : ℕ × ℕ | 2 ≤ nd.1 ∧ 2 ≤ nd.2 ∧ ExistsAME nd.1 nd.2} = oqp_35.answer

Category research open; AMS 05 Combinatorics, 15 Linear and multilinear algebra; matrix theory, 81 Quantum theory, 94 Information and communication, circuits. Declared in FormalConjectures/OpenQuantumProblems/35.lean, line 931.

Sources

• FormalConjectures/OpenQuantumProblems/35.lean at 2055e5ad
• https://oqp.iqoqi.oeaw.ac.at/existence-of-absolutely-maximally-entangled-pure-states

LeanOpenQuantumProblem35.ame_2_exists · OpenQuantumProblem35.ame_3_exists · OpenQuantumProblem35.ame_2_2_exists · OpenQuantumProblem35.ame_3_2_exists · OpenQuantumProblem35.ame_5_2_exists · OpenQuantumProblem35.ame_6_2_exists · OpenQuantumProblem35.ame_4_2_not_exists · OpenQuantumProblem35.ame_7_2_not_exists · OpenQuantumProblem35.ame_7_exists_iff · OpenQuantumProblem35.ame_4_3_exists · OpenQuantumProblem35.ame_4_6_exists · OpenQuantumProblem35.ame_7_6_open · OpenQuantumProblem35.ame_7_10_open · OpenQuantumProblem35.ame_8_4_open · OpenQuantumProblem35.ame_8_6_open · OpenQuantumProblem35.ame_8_10_open · OpenQuantumProblem35.ame_9_6_open · OpenQuantumProblem35.ame_9_10_open · OpenQuantumProblem35.ame_10_6_open · OpenQuantumProblem35.ame_10_10_open · OpenQuantumProblem35.ame_11_3_open · OpenQuantumProblem35.ame_11_4_open · OpenQuantumProblem35.ame_11_5_open · OpenQuantumProblem35.ame_11_6_open · OpenQuantumProblem35.ame_11_10_open · OpenQuantumProblem35.ame_12_5_open · OpenQuantumProblem35.ame_12_6_open · OpenQuantumProblem35.ame_12_10_open · OpenQuantumProblem35.oqp_35

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.