An AI system just spent nine weeks machine-checking a proof at the heart of one of quantum computing's landmark theorems.
The system, called FormalFlow, coordinates multiple AI proving agents under human supervision to tackle long-horizon formal verification, using a shared blueprint to manage nested planning, proving, and review loops. Researchers used it to produce a fully machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem underlying the MIP* = RE result in complexity theory. The job took 63 days and produced a library of 126,367 lines of Lean code, all generated by the agents themselves. Along the way, FormalFlow caught and corrected side conditions and intermediate errors in the original argument, while keeping the published final error bound intact under the corrected assumptions.
Formalizing a proof this size has historically taken specialist human teams years, which is why so few landmark results ever get the machine-checked treatment. If a small team with AI agents can do this kind of job in about two months, that changes the economics of verification for the dense, error-prone mathematics underpinning fields like quantum complexity theory. It also makes a quieter point: even a proof rigorous enough to publish still had side conditions worth fixing once every line was forced through a checker.
126,367 lines of AI-generated Lean code is an achievement, but it is also exactly the kind of pile that needs outside eyes before anyone treats it as gospel.