{"id":"palomar/PALOMAR-2026-11-02-000014","url":"https://github.com/zblore/fc-ame-12-5/tree/e8c1e58c7e4dd324868b6ed6a4ce59b103e2797f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-02-000014-v1.json","repo":"https://github.com/zblore/fc-ame-12-5","tags":["quant-ph","msc:81P40","msc:05C50"],"score":0,"title":"An absolutely maximally entangled state of twelve five-level systems: AME(12, 5) exists","trust":"high","domain":"quant-ph","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"quant-ph","summary":"A machine-checked proof that an absolutely maximally entangled state of twelve five-level systems exists. The statement and definitions are Formal Conjectures' (Open Quantum Problem 35, `ame_12_5_open`), copied verbatim into Challenge.lean, so this entry proves Formal Conjectures' own statement; one proof step inside the definition combineFirst is changed so that Comparator can match it, and the definition is unchanged. The witness is the graph state of the AME(12, 5) graph of S. Bevins and Y. Bidav. The proof is a general graph-state criterion over ZMod 5 plus 924 kernel-checked cut…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-11-02","reactions":{},"formalized":true,"formalizes":[{"title":"Symmetry-guided constructions of absolutely maximally entangled states in five open cases","identifier":"https://arxiv.org/abs/2608.05781","relationship":"formalizes"},{"title":"AME-paper-materials (the authors' reproducibility package)","identifier":"https://github.com/sjbevins/AME-paper-materials/tree/3fd8edc5bfc505e512c7a0c6168f92b44019f142","relationship":"formalizes"}]}