TY  - RPRT
TI  - Long-horizon autoformalization of a core theorem underlying MIP* = RE
AU  - Sirui Lu
AU  - Ruixuan Deng
AU  - David Zhu
AU  - Zhengfeng Ji
PY  - 2026
UR  - https://arxiv.org/abs/2609.19814
ID  - 2609.19814
ER  -