Long-horizon autoformalization of a core theorem underlying MIP* = RE.

arXiv:2609.19814v3 Announce Type: replace-cross Abstract: Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to address statement drift