A collaborative Lean 4 formalization of the theorem MIP* = RE (Ji, Natarajan, Vidick, Wright, Yuen, arXiv:2001.04383). The main theorem is stated, self-contained on top of Mathlib, in MIPRE/HaltingGameValue.lean: 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.

Upstreaming dashboard

This project will typically want to contribute some files into Mathlib itself. These files, which we can call ‘upstreaming candidates’, exist in this repository while they are being developed. This dashboard shows upstreaming candidates that look ready to ingest into Mathlib, and also files in the project that look “easy to unlock” for upstreaming.

For the dashboard to be correct, the repository must follow the same directory and filename structure as Mathlib for their upstreaming candidates. Namely, the upstream candidate A/B/C.lean, should exist in Mathlib/A/B/C.lean.

The dashboard highlights any open PRs to the Mathlib repository containing the corresponding files.

Upstreaming dashboard

Files ready to upstream

The following files are sorry-free and do not depend on any other file, meaning they can be readily PRed to Mathlib.

Files easy to unlock

The following files do not depend on any other file but still contain sorry, usually indicating that working on eliminating those sorries might unblock some part of the project.

Links