What was already known
Ji, Natarajan, Vidick, Wright and Yuen established MIP* = RE in 2020. This project builds on existing low-degree-test and parallel-repetition formalizations.
AI involvement
Claude Code wrote most Lean proofs against a human-directed manuscript and blueprint. Vidick reviewed contributions and made the modelling decisions; reused formalizations are credited.
Vidick and collaborators supplied the manuscript, blueprint and modelling choices; Claude wrote formal proof code for that human mathematics.
Importance
Makes a substantial known theorem and its reductions machine-checkable through a documented formal development.
Limitations
The verifier uses a tree-program model of polynomial time; equivalence with the paper’s Turing-machine model is cited but not formalized. Unused unfinished declarations are outside the checked theorems’ dependency trails. This is formalization of known mathematics, not a newly discovered theorem. AIProofWatch has not rebuilt the formal development or audited the complete proof. Palomar reports mechanical checking of a pinned statement; its automated statement review is not human peer review. The reported date records this registry checkpoint; the earlier first-report date of the formalization has not been established.
Technical verification
Reported is the default when evidence for a higher level is insufficient. No qualifying AI mathematical contribution remains in the proposed scope. Existing checks of the human result or its translation are retained as current evidence, without transferring them to an invented included AI contribution.
Formal checking
Registry-reported Comparator and kernel checking; not reproduced by AIProofWatch.
- Checker
- Palomar: Lean, NanoDa and con-ron (reported)
- Scope
- MIPRE.Palomar.mipstar_eq_re, halting_reduces_to_value, syncValue_uncomputable and quantumValue_uncomputable at 7798a80300e1c63b783c214f9e0cd9c00a8721b6, in the disclosed tree-program model; only the three standard Lean axioms.
- Basis
- Reported by the linked checker
- Check date
- 2026-10-08
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. No sufficient account of a named human explaining the scoped central reasoning is established in this assessment. Missing disclosure is not evidence of little understanding.
Correction and publication history
Source-statement, baseline, AI-role and verification-scope review, 14 October 2026. New curated contribution; eligible for matching consented digests.
Read this published revision