@misc{lu2026long,
title = {{Long-Horizon Autoformalization of a Core Theorem Underlying MIP*=RE}},
author = {Lu, Sirui and Deng, Ruixuan and Zhu, Yanqiao and Ji, Zhengfeng},
year = 2026,
eprint = {2609.19814},
archivePrefix = {arXiv},
primaryClass = {quant-ph},
}