aiqbench analysis
This article details FormalFlow, an AI system that successfully generated a machine-checked Lean 4 proof for a core theorem underpinning the MIP* = RE conjecture in quantum complexity theory. By coordinating proving agents with human supervision, the system produced over 126,000 lines of verified code in 63 days, offering a scalable path for small teams to validate major mathematical foundations without decades-long specialist efforts. The work demonstrates a significant convergence where AI automation directly advances fundamental research in quantum information science.
Long-horizon autoformalization of a core theorem underlying MIP* = RE
arXiv:2609.19814v1 Announce Type: new 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 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. Agents strengthen verification and review throughout formalization. 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. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.
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 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. Agents strengthen verification and review throughout formalization. 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. Developing the proof took 63 days; greater parallelism could further reduce this time. The final library contains 126,367 lines of Lean code, all generated by agents. The formalization corrects side conditions and intermediate errors while preserving the published final error bound under corrected assumptions. This work provides a verified foundation for quantum complexity and demonstrates a route to affordable verification of major research proofs by small teams.
72 pages. Main text 13 pages with 4 figures and 1 table, followed by supplementary appendices (57 pages, 9 figures, 17 tables) and references. Lean 4 library: this https URL
Quantum Physics (quant-ph); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
arXiv:2609.19814 [quant-ph]
(or arXiv:2609.19814v1 [quant-ph] for this version)
https://doi.org/10.48550/arXiv.2609.19814 arXiv-issued DOI via DataCite (pending registration)
Full text under the publisher's open licence · 207 words
Related coverage
[AINews] Opus 5.5 is good at explainer videos
Latent Space · Sep 29, 2026
[AINews] The Future of Latent Space
Latent Space · Sep 25, 2026
LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
arXiv · Jun 6, 2026
Synthesis Superintelligence: from Semiconductors to Superconductors — Periodic Labs’ Liam Fedus and Ekin Dogus Cubuk
Latent Space · Oct 8, 2026