{"id":"palomar/PALOMAR-2026-11-02-000010","url":"https://github.com/zblore/fc-ame-7/tree/974bf30aa49e4bf4b1d8f0be2eb22b9ce02cde42","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-02-000010-v1.json","repo":"https://github.com/zblore/fc-ame-7","tags":["quant-ph","msc:81P40","msc:81P45","msc:05B15"],"score":0,"title":"Absolutely maximally entangled states of seven parties: for d >= 2, AME(7, d) exists exactly when d >= 3","trust":"high","domain":"quant-ph","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"quant-ph","summary":"Machine-checked proofs that no absolutely maximally entangled state of seven qubits exists, and that for local dimension d >= 2 an absolutely maximally entangled state of seven parties exists exactly when d >= 3. The statements and definitions are Formal Conjectures' (Open Quantum Problem 35), copied verbatim into Challenge.lean, so this entry proves Formal Conjectures' own statements; one proof step inside the definition combineFirst is changed so that Comparator can match it, and the definition is unchanged. The proofs follow Huber, Gühne and Siewert (2017) and Shi, Zhang, Zhao and Li…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-11-02","reactions":{},"formalized":true,"formalizes":[{"title":"Absolutely maximally entangled states of seven qubits do not exist","identifier":"https://arxiv.org/abs/1608.06228","relationship":"formalizes"},{"title":"Constraints on correlations in multiqubit systems","identifier":"https://arxiv.org/abs/1710.00758","relationship":"adapts"},{"title":"Complete Existence Classification of Seven-Partite Absolutely Maximally Entangled States","identifier":"https://arxiv.org/abs/2608.01011","relationship":"formalizes"}]}