FormalFlow uses supervised AI to formalize a theorem behind MIP* = RE
A September 17 preprint reports a Lean 4 proof of a key quantum soundness theorem, developed over 63 days.
Making a long proof checkable
AI-assisted formalization has reached another research-scale test. In a September 17 preprint, Sirui Lu, Ruixuan Deng, Yanqiao Zhu and Zhengfeng Ji introduce FormalFlow, which coordinates proving agents around a shared plan with human oversight.
The team reports completing a Lean 4 proof of the quantum soundness of the classical low individual-degree test in 63 days. This is a supporting theorem for MIP* = RE; the project does not formalize that entire result.
Their account highlights a practical difficulty: code can compile while representing the wrong mathematical claim. Repeated review therefore checks both proof dependencies and the meaning of statements. The authors report correcting assumptions and intermediate errors while retaining the published final error bound under the corrected assumptions.
For mathematical research, the value is a proof that others can inspect and check. These are preprint claims; MathsAI has not independently rebuilt the released library.