Long-horizon autoformalization of a core theorem underlying MIP* = RE

arXiv:2609.19814 · quant-ph, cs.AI, cs.LO · Submitted 2026-09-17 · Read on arXiv

quant-ph, cs.AI, cs.LO

Submitted: 2026-09-17

Updated: 2026-09-24

Comments: 72 pages. Main text 13 pages with 4 figures and 1 table, followed by supplementary appendices (57 pages, 9 figures, 17 tables) and references. Lean 4 library: https://github.com/LionSR/MIPStarRE

Code: https://github.com/LionSR/MIPStarRE

Project page: https://imperialcollegelondon.github.io/FLT

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Consistency — 63× in this paper · explained in 3 episodes
• Verification — 23× in this paper · explained in 2 episodes
• Trace — 20× in this paper · explained in 2 episodes
• Axioms — 15× in this paper · explained in 2 episodes
• Scaffolding — 11× in this paper · explained in 3 episodes
• Core — 8× in this paper · explained in 2 episodes
• Hilbert Space — 5× in this paper · explained in 2 episodes
• Task Planning — 4× in this paper · explained in 2 episodes
• Adam — 3× in this paper · explained in 2 episodes
• Alignment — 3× in this paper · explained in 1 episode
• Task Decomposition — 3× in this paper · explained in 2 episodes
• AI Agents — 2× in this paper · explained in 2 episodes
• Embeddings — 2× in this paper · explained in 2 episodes
• Entanglement — 2× in this paper · explained in 4 episodes
• Reinforcement Learning — 2× in this paper · explained in 4 episodes
• Abstraction — 1× in this paper · explained in 1 episode
• Adaptation — 1× in this paper · explained in 1 episode
• Aggregation — 1× in this paper · explained in 1 episode
• Approximation Bound — 1× in this paper · explained in 1 episode
• Benchmark — 1× in this paper · explained in 2 episodes
• Decoupling — 1× in this paper · explained in 2 episodes
• Failure Modes — 1× in this paper · explained in 3 episodes
• Fidelity — 1× in this paper · explained in 2 episodes
• Semidefinite Programming (SDP) — 1× in this paper · explained in 3 episodes
• Steering — 1× in this paper · explained in 2 episodes

Sources

• Quantum soundness of the classical low individual degree test
• Generative Language Modeling for Automated Theorem Proving
• DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
• Formalizing Mathematics at Scale
• Advancing Mathematics Research with AI-Driven Formal Proof Search
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
• MIP*=RE
• Three-player entangled XOR games are NP-hard to approximate
• The Verification Horizon: No Silver Bullet for Coding Agent Rewards
• Concrete Problems in AI Safety
• Multi-agent Autoformalization of Tensor Network Theory

Related papers

• Reconquering Bell sampling on qudits: stabilizer learning and testing, quantum pseudorandomness bounds, and more
• Encrypted clones can leak: Classification of informative subsets in Quantum Encrypted Cloning
• Polynomial-time classical and quantum simulation of quantum impurity models
• Theory of quantum-enhanced interferometry with general Markovian light sources
• A convergent hierarchy of spectral gap certificates for qubit Hamiltonians
• Universal Bound and Phase Transition in Many-Body Fermionic Non-Gaussianity