Primary evidence
- Long-horizon autoformalization of a core theorem underlying MIP* = RES1 · Primary research · Paper · 2026-09-17
- MIPStarRE Lean formalization repositoryS1 · Primary research · Formal artifact
FormalFlow completes a 126,000-line Lean formalization of a core theorem underlying MIP* = RE
FormalFlow organizes long formalization projects around a shared blueprint and nested planning, proving and review loops. AI agents implement and review proof tasks while humans supervise the project, compare the formal development with the source mathematics and resolve semantic discrepancies.
What happened?
The FormalFlow team reported a complete machine-checked Lean 4 proof of the quantum soundness of the classical low individual-degree test, a core theorem used in the MIP* = RE line of work. The paper reports that the development took 63 days, contains 126,367 lines of Lean code generated by AI proving agents, and corrected several side conditions and intermediate errors while preserving the published final error bound under corrected assumptions.
FormalFlow organizes long formalization projects around a shared blueprint and nested planning, proving and review loops. AI agents implement and review proof tasks while humans supervise the project, compare the formal development with the source mathematics and resolve semantic discrepancies. The public MIPStarRE repository preserves Lean sources, the active blueprint, source-paper material and CI-oriented proof-integrity infrastructure.
Why it matters
Large research proofs expose failure modes that short theorem-proving benchmarks do not: statement drift, dependency management, incompatible local lemmas and review debt. FormalFlow provides evidence that agentic workflows can sustain a research-scale formalization over months while using the Lean kernel as a final syntactic proof checker and additional project processes to audit semantic fidelity.
Significance rationale: FormalFlow is a field milestone in long-horizon AI-assisted formalization because it reports completion of a machine-checked Lean development for the quantum soundness theorem of the classical low individual-degree test, a technically central ingredient underlying MIP* = RE. The project required 63 days and produced 126,367 lines of Lean code generated by proving agents under human supervision, demonstrating sustained proof planning, composition and review far beyond isolated theorem-hole solving while stopping short of a new mathematical theorem.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Human–AI collaboration
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Formalization of known result
- Interface
- Formal, Hybrid
- AI contribution
- The paper states that the Lean library was generated by AI proving agents coordinated through FormalFlow, while humans supervised the project and intervened in planning, source-faithfulness review and resolution of proof or statement gaps.
- Human contribution
- Human researchers designed and supervised the workflow, selected and interpreted the source theorem, maintained the blueprint and review process, and adjudicated semantic discrepancies between the paper and the formal development.
- Verification
- Paper released · E3 · Inspectable artifact · Machine-checked
- Last reviewed
- 2026-09-27
Technical details
- Systems
- formalflow, lean
- Organizations
- —
- Problems
- mip-star-equals-re, low-individual-degree-test
- Methods
- long-horizon-autoformalization, multi-agent-proof-development, blueprint-guided-formalization, formal-verification
Sources & artifacts
- Long-horizon autoformalization of a core theorem underlying MIP* = RES1 · Primary research · Paper · accessed 2026-09-27
- MIPStarRE Lean formalization repositoryS1 · Primary research · Formal artifact · accessed 2026-09-27
- MIPStarRE Lean 4 developmentArtifact · Proof artifact
Verification history
- 2026-09-17 · Paper released · E3 · Inspectable artifact
The arXiv paper reports a completed machine-checked Lean 4 formalization and the public MIPStarRE repository exposes the corresponding Lean project and proof development infrastructure. Chronicle has not located an independent replay of the release artifact in this maintenance pass.
Corrections
No corrections recorded.