{"id":"arxiv/2609.19814","url":"https://arxiv.org/abs/2609.19814","tags":["quant-ph","cs.AI","cs.LO"],"score":0,"title":"Long-horizon autoformalization of a core theorem underlying MIP* = RE","domain":"quant-ph","source":"arxiv","authors":["Sirui Lu","Ruixuan Deng","Yanqiao Zhu","Zhengfeng Ji"],"reviews":0,"subject":"quant-ph","summary":"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 and proof composition in long-horizon formalization. Drawing on software-engineering principles and practices, it uses a shared blueprint to guide nested planning, proving, and review loops. Using FormalFlow, we completed a machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE, in 63 days. The final library…","category":"research","comments":0,"disputed":false,"division":"physics","mentions":0,"discussed":0,"published":"2026-09-17","reactions":{}}