{"id":"palomar/PALOMAR-2026-10-09-000012","url":"https://github.com/vidick/MIPRE-formalization/tree/7798a80300e1c63b783c214f9e0cd9c00a8721b6","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-09-000012-v1.json","repo":"https://github.com/vidick/MIPRE-formalization","tags":["quant-ph","cs.CC","msc:68Q15","msc:81P45","msc:03D35","msc:46L10","quantum-information","nonlocal-games","computability","lean"],"score":0,"title":"MIP* = RE","trust":"high","domain":"quant-ph","source":"palomar","authors":["Thomas Vidick"],"reviews":0,"subject":"quant-ph","summary":"A Lean 4 formalization of MIP* = RE (Ji, Natarajan, Vidick, Wright and Yuen): the class of languages decidable by a classical polynomial-time verifier interacting with two provers who share entanglement, with completeness 1 and soundness 1/2, is exactly the class of recursively enumerable languages. The development also contains the halting reduction behind it (a computable map from Turing machines to nonlocal games whose synchronous and quantum values are 1 if the machine halts and at most 1/2 otherwise) and its corollaries that the synchronous and the quantum value of a game are…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"verified":true,"discussed":0,"published":"2026-10-09","reactions":{},"formalized":true,"formalizes":[{"title":"MIP* = RE","identifier":"arXiv:2001.04383","relationship":"formalizes"}]}