MIP* = RE — a Lean formalization project

This repository hosts a collaborative Lean 4 formalization project for the theorem MIP* = RE (Ji, Natarajan, Vidick, Wright, Yuen, arXiv:2001.04383).

A Mathlib-only statement of the main theorem is in MIPRE/HaltingGameValue.lean (HaltingGameValue.HaltingReducesToGameValue): there is a computable map from Turing machines to nonlocal games sending halting machines to games of synchronous value 1 and non-halting machines to games of value at most 1/2.

Status. That statement is proved: HaltingGameValue.halting_reduces_to_gameValue, with no sorry and no axiom beyond propext, Classical.choice and Quot.sound. The proof lives in MIPRE/MainTheorem.lean, because it needs the whole development and the statement file imports Mathlib only. The same file proves the reduction to the quantum value, the uncomputability of both values, and MIPRE.Halting.mipstar_eq_re : MIPStar = IsRE for the paper's polynomial-time class (MIPRE.MIPStar; the computable relaxation is MIPRE.MIPStarComputable, with mipstarComputable_eq_re).

Registered. The result is registered in the Palomar registry of Lean-verified mathematics as PALOMAR-2026-10-09-000012 (2026-10-09, commit 7798a80). Palomar rebuilt the project in a fresh environment, compared the Mathlib-only statements of Palomar/Challenge.lean with the proofs of Palomar/Solution.lean through lake comparator, and replayed the proofs through Lean's kernel and two independent checkers; its automated editorial review found no problem.

The proof is the compression pipeline (MIPRE.GapCompression.ofPipeline) with its three stages supplied:

• introspection, MIPRE.Introspection.seven;
• answer reduction, MIPRE.AnswerReduction.answerReduction, over the classical PCP decider;
• parallel repetition, repetition 7.

The Aldous–Lyons conjecture. The development also proves the main theorem of The Aldous–Lyons Conjecture II: Undecidability (Bowen, Chapman, Vidick, arXiv:2501.00173), TMIP* = RE, as the Mathlib-only statement TailoredGameValue.TailoredHaltingReduction, and with it the corollary of The Aldous–Lyons Conjecture I: Subgroup Tests (Bowen, Chapman, Lubotzky, Vidick, arXiv:2408.00110) that the Aldous–Lyons conjecture is false, SubgroupTestValue.aldous_lyons_false : ¬ AldousLyons (MIPRE/SubgroupTestValue.lean). Both are proved in MIPRE/TailoredMIP.lean, with the same three axioms; the plan was planning/aldous-lyons-track.md.

Project links

• Project website
• Palomar entry PALOMAR-2026-10-09-000012 — the registered, independently verified record
• Blueprint — the proof plan, with a dependency graph linking informal mathematics to Lean declarations
• API documentation
• Task dashboard — see CONTRIBUTING.md for how to claim a task
• Independent verification with the Lean comparator, each in a repository whose only file to audit is a Mathlib-only Challenge.lean: mipre-comparator for the halting reduction of MIP* = RE, and aldous-lyons-comparator for TMIP* = RE and the refutation of the Aldous–Lyons conjecture

Building the project

1. Install Lean 4 following the Lean installation guide (this installs elan and VS Code support).
2. Clone this repository and fetch the Mathlib build cache — do not build Mathlib from source:

   git clone https://github.com/vidick/MIPRE-formalization.git
   cd MIPRE-formalization
   lake exe cache get
   lake build
   

For native Windows development, see the local Lean workflow for caches outside OneDrive and timed single-file, module, and full-library checks.

Cloud sessions

Claude Code cloud sessions on this repository get Lean 4, a compiled Mathlib and this repository's own compiled modules — the latter published by CI on every push to main and downloaded into the environment's snapshot by its setup script (.claude/cloud-setup.sh), since nothing can be compiled inside the five minutes a setup script gets. A SessionStart hook and the lean-lsp MCP server expose all of it to the session's checkout; see docs/lean-cloud.md for the one-time environment configuration.

Building the blueprint locally (optional)

The blueprint is compiled by CI on every push to main, so you do not need a local setup to contribute. If you want a local preview (requires a TeX distribution and leanblueprint):

pip install leanblueprint
leanblueprint pdf    # -> blueprint/print/print.pdf
leanblueprint web    # -> blueprint/web/   (requires graphviz/pygraphviz)
leanblueprint serve  # preview the website locally

Repository layout

• MIPRE/ — the Lean source files (MIPRE.lean is the root module importing everything).
  • MIPRE/Mathlib/ — general-purpose declarations destined to be upstreamed to Mathlib (tracked on the upstreaming dashboard).
  • MIPRE/LCS/ — binary linear constraint system (LCS) games, contributed by Sean Perazzolo (vendored with permission from sean-prz/LCS_In_Lean and adapted to this repository: Lean/Mathlib v4.32.0, ZMod 2 outcome types, Mathlib naming conventions): observable and projector strategies, loss operators and their sum-of-squares decomposition, solution groups, the Mermin–Peres magic square, and a bridge interpreting an LCS instance as a MIPRE.Game (MIPRE/LCS/NonlocalGame.lean).
  • MIPRE/Background/LIDT/ — the classical low individual degree test. Its soundness theorem is the one formalized by Sirui Lu, Ruixuan Deng and Zhengfeng Ji in MIPStarRE, which lakefile.toml requires as a Lake dependency at a pinned commit (registered in Palomar as PALOMAR-2026-08-18-000001; see planning/palomar-dependencies.md). The directory states the theorem in this repository's vocabulary and bridges the two (Bridge/), and Co/ ports the proof to commuting-operator strategies; the plan is in .

Contributing

See CONTRIBUTING.md for the full workflow (task claiming, pull requests, review cycle). The blueprint's introduction describes entry points by background (quantum information, complexity/computability, operator algebras, Lean/Mathlib), and required external results are tagged with effort estimates (easy / medium / hard / in Mathlib) in the blueprint.

Acknowledgements

This repository is based on the LeanProject template and copies its collaboration mechanisms from the FLT project.