Open Quantum Problem 35: existence of absolutely maximally entangled pure states

The question

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

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

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

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

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

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

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

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

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

oqp_35. 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.

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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OpenQuantumProblems.«35» (10 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem ame_8_4_open :
    answer(sorry) ↔ ExistsAME 8 4

theorem ame_8_6_open :
    answer(sorry) ↔ ExistsAME 8 6

theorem ame_8_10_open :
    answer(sorry) ↔ ExistsAME 8 10

theorem ame_10_6_open :
    answer(sorry) ↔ ExistsAME 10 6

theorem ame_10_10_open :
    answer(sorry) ↔ ExistsAME 10 10

theorem ame_11_3_open :
    answer(sorry) ↔ ExistsAME 11 3

theorem ame_11_6_open :
    answer(sorry) ↔ ExistsAME 11 6

theorem ame_12_6_open :
    answer(sorry) ↔ ExistsAME 12 6

theorem ame_12_10_open :
    answer(sorry) ↔ ExistsAME 12 10

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

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

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.

Source and licence

Imported from Formal Conjectures (Open quantum problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.