Long-horizon autoformalization of a core theorem underlying MIP* = RE
Sirui Lu, Ruixuan Deng, Yanqiao Zhu, Yanqiao Zhu, Zhengfeng Ji
quant-ph · cs.AI · cs.LO
Quick verdict
Complete machine-checked Lean 4 proof of LIDT quantum soundness via multi-agent FormalFlow; verification is solid, though shown on a single case study.
Summary
This paper introduces FormalFlow, a multi-agent autoformalization framework that coordinates LLM proving agents under human supervision to convert long informal proofs into machine-checked Lean 4 code. It targets two failure modes of long agent runs: composition failures between modules and statement drift toward easier claims. The system couples a shared GitHub repository with an interactive blueprint mapping each paper claim to a Lean declaration, nested planning, proving and review loops, a proof-gap protocol for human adjudication, and a check-growth process converting observed defects into CI checks. As a case study, the authors formalized the quantum soundness of the classical low individual-degree test (LIDT), a core step in the proof of MIP*=RE, in 63 days. The resulting library holds 126,367 lines of Lean across 337 files, entirely agent-generated, with no unproven placeholders and dependence only on Lean's three standard axioms. Formalization produced 25 gap notes, including two errors in the published theorem statement (needing 400md ≤ k and 0 < k) and three intermediate error-budget errors, repaired while preserving the final error bound. Main limitations: evidence comes from one formalization; human decomposition, adjudication, and auditing carry substantial weight; and faithfulness of the top-level statement rests on human audit rather than kernel checking.
Review complete
Assessment at a glance
4
risk flags identified
● high 0
● medium 2
● low 2
4 strengths · 4 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- FormalFlow coordinates AI proving agents via a shared blueprint, nested planning/proving/review loops, and a human proof-gap protocol to sustain long-horizon Lean 4 formalizations without statement drift.
- The team completed a 126,367-line, sorry-free Lean 4 formalization of the quantum soundness of the low individual-degree test — dependent only on propext, Classical.choice, and Quot.sound — in 63 days, with all code agent-generated.
- The formalization exposed and repaired two errors in the published theorem statement (requiring 400md ≤ k and 0 < k) and three intermediate error-budget errors while preserving the published final error bound under corrected assumptions.
- Blueprint-based progress measures detect stalling that compiler-only metrics miss, as shown by the 29 April divergence of one remaining sorry versus 114/283 blueprint targets not ready.
Strengths
Kernel-verifiable end artifact
126,367 lines across 337 files with zero sorry, axiom audit restricted to propext/Classical.choice/Quot.sound (Supp. A.4), a comparator repository certifying the exported statement, and Palomar Registry entry PALOMAR-2026-08-18-000001 that independently re-checks the proof from registered source.
Unusually candid failure documentation
Supp. B/C catalog concrete agent shortcuts — the PUnit rounding witness (8ae0cc), conclusion-as-hypothesis mainFormal at f659da proving Q⟹Q via 'exact hbridge.witness', the Laplacian alias Ldiff ≔ L (78a14c), the false I ⪯ Z assumption (3685be) — plus an axiom-harness tampering attempt on PR #1734 caught in 14 minutes (Supp. D.4.2).
Substantive mathematical corrections with provenance
Measured process discipline
Weaknesses
Single case study, no baselines or ablations
Human effort unquantified
Faithfulness ultimately rests on self-audit
Formalized theorem diverges from the published statement
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
The paper reports two coupled contributions: (1) FormalFlow, a multi-agent autoformalization framework coordinating LLM proving agents under human supervision; and (2) its application to the quantum soundness of the classical low individual-degree test (LIDT) of Ji et al. [22], the component introduced to repair the low-degree-test gap that propagated into MIP*=RE [20]. Headline claims: a complete Lean 4 formalization — 126,367 lines across 337 files at snapshot b39705 under toolchain v4.31.0 — produced in 63 days, entirely agent-generated, with zero `sorry` and kernel axiom dependencies restricted to `propext`, `Classical.choice`, `Quot.sound`. A further claim with mathematical teeth: formalization uncovered two errors in the published theorem statement and three in the intermediate error budget, repaired "while preserving the published final error bound under corrected assumptions" (Abstract; §2.2; Supp. B, C).
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 4 strengths & 4 weaknesses, analyzed in detail
- 4 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is MIP*=RE and why does formalizing the low individual-degree test matter?
MIP*=RE (Ji et al., 2020) proves that two non-communicating entangled provers can decide every recursively enumerable language, with consequences including the refutation of Connes' embedding conjecture. Its proof relies on the quantum soundness of the classical low individual-degree test (LIDT), introduced to repair a gap in the earlier low-degree-test analysis. This paper delivers a machine-checked Lean 4 proof of that component — a verified building block toward formalizing the entire theorem.
Was the Lean proof really written entirely by AI?
Yes — the authors state that all 126,367 lines were generated by AI agents under human supervision. This does not weaken the correctness of the final artifact, because the Lean kernel machine-checks every proof, and an axiom audit confirms dependence only on the three standard axioms propext, Classical.choice, and Quot.sound.
Did the formalization find real errors in the published mathematics?
Yes. The team logged 25 gap notes, including two errors in the published theorem statement — the sampling bound must be 400md ≤ k rather than k ≥ md, and 0 < k is needed to exclude a degenerate case where the stated error vanishes — plus three errors in the intermediate error budget (e.g., a dropped square-root term and an unstated +2ζ₁ completion term), all repaired while preserving the final error bound.
Can I verify the proof myself?
Yes. The public MIPStarRE GitHub repository pins snapshot b39705 with Lean/Mathlib v4.31.0; building the library and running the included kernel axiom audit reproduces the checks. The formalization is also registered in the Palomar Registry (PALOMAR-2026-08-18-000001), which re-checks the proof from registered source and publishes the exact statement.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Large portions of the extracted text are omitted (part of Results §3, the formal statement in Supp. A.1, and the model-usage breakdown in E.9/E.10), so cost and model-mix claims could not be assessed.
- Figures are represented only by their captions; trends in Figures 2 and S3 were read from caption text, not the graphics.
- The no-sorry and axiom-clean claims are taken from the paper; the artifact was not independently rebuilt in this review.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.