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

Sirui Lu, Ruixuan Deng, David Zhu +2

Landmark mathematical formalizations have taken specialist teams years to complete. We present FormalFlow, a system that coordinates AI proving agents under human supervision to ad…