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.
Stellar Colosseum is introduced, a model-agnostic harness for allocating inference across research in mathematics and theoretical computer science that demonstrates the capabilities of Colosseum through open-ended research and evaluations on theorem-proving and competitive programming benchmarks.
Hong-Hao Lin, David P. Woodruff, Yuan Deng et al.· 2 citations· ⚡1
This work introduces ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction that autonomously constructs the Lean model and supporting theory.
Rosetta is presented, a multi-agent LLM pipeline that automatically generates first-principles analytical models from research paper PDFs, and four design decisions address failure modes of na\"ive LLM-based generation.
Prove2Me aims to turn math formalization into a scalable, crowd-sourced effort open to anyone with an agent, and designed mechanisms and a specialized harness that enable large-scale collaboration so that agents can build on one another's work and freely reuse existing results.
Shu-Ze Chen, Kunal Marwaha, Xiao-Yang Lu et al.· 3 citations
Proof-Sketch-Guided Formal Model Synthesis (ProGS), an autoformalization method centered on model-based proof sketches, which improves over state-of-the-art agentic formal modeling approaches in syntactic validity, deductive verifiability, and behavioral correctness.
Hong-Shu Wang, Xin-Yue Zuo, Yu-Fan Cai et al.· 0 citations
An anecdotal account of AI agents, equipped with a CLI and a proof assistant, producing thousands of lines of machine-checked code, and the role of the human expert, whose contribution reduces to providing natural-language problem descriptions, reviewing auto-generated specifications, and occasionally supplying a key i...
Eleftherios Ioannidis, Nikhil Swamy, Gabriel Ebner et al.· Proc. ACM Program. Lang.· 1 citation
Related blog posts
MIT News · Artificial Intelligence· news.mit.eduOct 6, 2026
Computer-use AI agents struggle with multi-step workflows like email and customer support. Echoverse trains agents in realistic environments rather than simply providing more training tasks, helping them improve as the tasks, tests, and environments evolve. The post Echoverse: Deep, evolving environments for computer-use agents appeared first on Microsoft Research.
Known for his clear and elegant writing style, Bertsekas shaped fields from control and optimization to large-scale computation and artificial intelligence.
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
