{"id":"d8108515-8cb1-48c2-a100-dc2b77baee10","arxiv_id":"2501.00173","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"TailoredMIP* = RE: every Turing machine is reduced to a tailored non-local game whose perfect strategy exists iff the machine halts, yielding the falsity of the Aldous-Lyons conjecture.","lead":"This paper proves that the problem of telling whether certain quantum puzzle games have a perfect winning strategy is undecidable. The result resolves the Aldous-Lyons conjecture in the negative and strengthens the earlier MIP*=RE theorem.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Answer reduction's tailored-structure preservation is the unproven crux: any encoded bit depending non-linearly on unreadable answers would break ZPC completeness or tailored soundness.","rationale":"I read the paper in good faith: it carefully sets up tailored games, normal form verifiers, and a clear reduction from the Halting Problem assuming Compression. The deduction in §2.6 is logically sound given Theorem 2.53 and Lemma 2.61; the fixed-point construction and the entanglement-lower-bound argument are standard. The reader's weakest_assumption correctly points to the Compression theorem's proof being deferred. My stress-test narrows this to the single most load-bearing sub-step: Answer Reduction's preservation of the tailored structure. The introduction itself flags this as the main difficulty ('any bit of the encoded answer that depends on an unreadable bit of the original answer must do so in a linear manner only'), and it is the place where the adaptation from [JNV+21] is least routine. Corollary 3.41 gives exactly the allowed operations on ZPC strategies, and the AND example in (27) shows the obstruction is real for unreadable bits. If the PCP somewhere requires a product of two unreadable bits, the completeness map would produce a non-permutation observable, breaking the ZPC condition, or the game would cease to be tailored. The soundness side is equally delicate: the low-degree test and consistency checks must not induce nonlinear equations on unreadable variables. This is not an observed error, but it is a specific, checkable condition. The reader's verdict CONDITIONAL remains appropriate: the paper should be accepted only if Sections 4–7 verify this linearity condition in full. I do not see grounds to reject or to accept outright without the missing proof.","tokens_in":63077,"tokens_out":6970,"duration_ms":71151,"concrete_test":"Isolate the Answer Reduction construction in §5 and verify it on a minimal TNFV with one unreadable answer bit and a decision predicate that combines an AND of two readable bits with the unreadable bit. Specifically, re-derive the definition of the encoded assignment (around Definition 5.2x) and check that every coordinate that depends on the unreadable bit is affine in it. If any coordinate is a product of two unreadable variables (e.g., x_L · y_L), the Reed–Muller encoding at total degree 2 would break the linearity requirement; show that no such product appears or is forced by the verifier's checks. Alternatively, implement the transformation on this two-vertex example and test whether every perfect ZPC strategy of the original game lifts to a perfect ZPC strategy of the encoded game.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim Theorem 2.31 is deduced from Compression (Theorem 2.53), whose proof is deferred to Sections 4–7. The most delicate step is Answer Reduction (§5, Theorem 5.1): it must output a tailored game in which every new answer bit that is a function of an original unreadable bit is an affine function of those bits, with all other checks confined to readable bits. Corollary 3.41 allows arbitrary functions of readable Z-aligned variables and affine functions of all variables, but the PCP encoding of the verification circuit of the oracularized game computes assignments to gate outputs, including AND (multiplication) of wire values. If a wire derived from an unreadable bit must be multiplied with another unreadable bit to verify a check, the resulting observable need not be a signed permutation — the four-dimensional counterexample near (27) in §3.4 demonstrates this. Therefore the completeness map from a perfect ZPC strategy of the original game to one for the encoded game would fail, and the tailored category would be lost. The authors assert that the Reed–Muller-based PCP is carefully designed so any bit depending on unreadable bits does so only linearly, but the proof is not present in the reviewed portion. This is exactly the non-routine adaptation of [JNV+21], where nonlinear dependence on answers is available. If the linearity constraint cannot be met for all gates in the Cook–Levin circuit, the soundness or completeness of Answer Reduction collapses, and with it the undecidability reduction.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims a negative resolution of the Aldous–Lyons conjecture (joint with the companion paper [BCLV24]) by proving TailoredMIP* = RE (Theorem 2.31): a polynomial-time map from Turing machines M to tailored non-local games G_M such that if M halts there is a perfect Z-aligned permutation strategy commuting along edges (ZPC), and if M never halts the synchronous quantum value is at most (claimed strictly less than) 1/2. The proof follows the MIP*=RE architecture: Section 2 derives Theorem 2.31 from a Compression Theorem (Theorem 2.53) by a fixed-point construction, and Compression is presented as the composition of question reduction, answer reduction, and parallel repetition, with proofs deferred to Sections 4–7. Section 3, included in the reviewed text, develops the technical toolbox: distances between strategies, data processing, a criterion for ZPC preservation (Corollary 3.41), game transformations, and the Pauli-basis self-test. The text under review contains Sections 1–3; the proofs of the three compression transformations are not present.","tokens_in":63379,"tokens_out":30722,"duration_ms":300205,"significance":"If the deferred proofs are correct, the result is of the first importance: it gives non-sofic unimodular networks (refuting Aldous–Lyons, via the reduction in [BCLV24]), reproves the negation of Connes' embedding problem (MIP*=RE) in a streamlined way, and establishes the stronger statement TailoredMIP* = RE with perfect strategies restricted to ZPC strategies. The visible portion is carefully written: the fixed-point construction and the deduction of Theorem 2.31 from Theorem 2.53 are explicit and mostly sound; Corollary 3.41 cleanly isolates the data-processing operations that preserve the tailored/ZPC category and is checkable from the material given; and the incorporation of simplifications from [dlS22b] and [Vid22] is a genuine strength. The significance is, however, conditional: the central technical contribution, a compression theorem that preserves the tailored structure, is asserted rather than proved in the reviewed text, and the paper itself identifies answer reduction as the delicate step. The present report therefore assesses the architecture and the visible deduction, not the full claim.","major_comments":[{"comment":"The main theorem is deduced from the Compression Theorem, but the proof of Compression is entirely deferred to Sections 4–7, which are not part of the text under review. The crux is Answer Reduction: as the introduction itself states in §1.1, the PCP must be designed so that \"any bit of the encoded answer that depends on an unreadable bit of the original answer must do so in a linear manner only,\" and the proof of this property (Theorem 5.1) is not given. This is precisely the point at which the tailored setting departs from [JNV+21], where nonlinear dependence on answers is available, and it is load-bearing: if any encoded bit depended nonlinearly on unreadable bits, the completeness map via Corollary 3.41 would fail (the counterexample near (27) in §3.4 shows that the AND of two non-Z-aligned signed permutations is not a signed permutation), and the output game would not be tailored. The same concern applies to Question Reduction for conditionally linear samplers, stated as Theorem 4.36. A complete draft containing these proofs must be provided before the central claim can be verified.","section":"§2.6.2 (Theorem 2.53); §5 (Theorem 5.1)"},{"comment":"The completeness argument contains a false inference: from n ≥ log N it concludes that 2n ≥ N, which is not true in general (e.g., if N = 2^10 and n = 10, then 2n = 20 < 1024). The correct threshold is N/2: from perfect ZPC strategies for V_{2n} with 2n ≥ N one obtains perfect ZPC strategies for V_n with n ≥ N/2, and iterating gives V_C after about log_2(N/C) halving steps. The iterated-logarithm chain in the text (\"log N\", \"log log N\", ...) is inconsistent with the factor-of-two index change in Theorem 2.53 and must be replaced by iterated halving. The conclusion is recoverable, but the proof as written is incorrect.","section":"§2.6.3, proof of Theorem 2.31 (completeness case)"},{"comment":"Lemma 2.61 is load-bearing: it is used to show both that V_{M,λ} is λ-bounded (so that Theorem 2.53 applies) and that the sampler and linear-constraints processor of G_M run in time poly(|M|). Its proof is only a sketch, ending with the suggestion that \"it is probably better for the readers to try and follow these calculations for themselves,\" and the details are referred to [JNV+21, Lemma 12.5]. Since the present paper changes the verifier model (tailored normal form verifiers with a fixed canonical decider, and the specific fixed-point machine F of Definition 2.56), the revision should contain the full accounting argument rather than a pointer to the prior literature.","section":"§2.6.3, Lemma 2.61"}],"minor_comments":[{"comment":"The soundness iteration establishes only E(V^{M,λ}_C, 1/2) = ∞, which implies val*(G_M) ≤ 1/2; the strict inequality claimed in Theorem 2.31(3) does not follow from this, because the supremum defining val* need not be attained by any finite-dimensional strategy. Theorem 1.1 and the informal definition of TailoredMIP* in §2.6 use the threshold ≤ 1/2; the statements should be aligned, or an additional argument for the strict inequality should be supplied.","section":"Theorem 2.31(3) and its proof"},{"comment":"Definition 2.56 says F runs M for n steps and returns the empty tape if it halts, while Lemma 2.59(3) and Corollary 2.60(1) are phrased as \"halts in less than n steps\" and \"halts in n steps\"; these should consistently read \"halts within n steps\" to match the semantics of the machine F.","section":"Definition 2.56; Lemma 2.59(3); Corollary 2.60(1)"},{"comment":"Claim 3.16 states that corners of PVMs are ε-almost projective, but the proof gives the slightly weaker bound (1 + 2ε)ε, since the deficiency bound τ(Id − ωω*) ≤ ε is taken with respect to the M-dimensional normalized trace while the 1-norm in the conclusion is N-dimensional. Subsequent uses absorb constants, so this is a precision issue rather than a substantive error, but the parameter should be adjusted.","section":"Claim 3.16"},{"comment":"The manuscript contains numerous typos that a copyedit pass should fix: \"proivde\" in §1.2, \"mononid\" in Remark 1.3, \"obejcts\" in Remark 2.19, \"sarisfied\" and \"constriants\" in Example 2.29, \"commonlu\" in Definition 3.30, and \"Scwhwartz\" in the proof of Claim 3.18.","section":"Throughout"},{"comment":"The displayed chain of inequalities contains broken underbrace macros rendered literally as \"bracehtipupleft/bracehtipdownright,\" which makes the chain difficult to read; the source should be repaired.","section":"§2.6.3, displayed iteration in the proof of Theorem 2.31"}],"recommendation":"major_revision","confidential_remarks":"The text provided for review contains only Sections 1–3 plus the table of contents; the proofs of Sections 4–7, which contain the Compression Theorem and its three component transformations, are absent. If the full arXiv submission does contain these sections, the editor should send the complete text for review, since the present assessment is necessarily conditional on an unverified theorem. The paper is explicitly one of a two-part series, and the headline implication for Aldous–Lyons depends on the companion paper [BCLV24]; the present manuscript should ultimately be judged on the strength of its own claim, TailoredMIP* = RE. The errors noted in §2.6.3 (the incorrect log N threshold in the completeness case and the uninferred strict inequality in the soundness case) suggest that the final version needs a careful revision of the fixed-point argument, and the deferred proof of Lemma 2.61 should be included in full rather than pointed to in [JNV+21]."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"First: this is real work on a major problem. The main theorem—TailoredMIP*=RE—is a strict strengthening of MIP*=RE, and if the companion reduction holds, it refutes Aldous–Lyons. The high-level deduction of Theorem 2.31 from the Compression Theorem is explicit, careful, and I could not find a gap in the fixed-point argument or the entanglement lower bound iteration. The introduction of tailored games as a controlled-linear class between LCS and synchronous games is a genuinely useful framing, and Corollary 3.41 (affine data processing preserves Z-aligned signed permutations) is a clean tool.\n\nThe soft spot is exactly where the reader and stress-test put it: the Compression Theorem is the load-bearing component, and its proof is deferred to Sections 4–7. The answer-reduction step must preserve the tailored structure—specifically, any encoded bit that depends on an unreadable answer bit must be affine in those bits, while all AND-gates are confined to readable bits. The authors state this is achieved by a bespoke Reed–Muller-based PCP, and they describe the obstacle (AND of unreadable bits would produce observables that are not signed permutations, as in (27)). I cannot verify that from the first three sections; the actual PCP construction and analysis are not in the reviewed portion. This is a deferral, not an observable error, but it is a big deferral. A referee should spend serious effort on Section 5, especially Theorem 5.1 and the linearity argument for unreadable wires.\n\nMinor: Lemma 2.61 is given as a proof sketch with a reference to JNV+21 Lemma 12.5; that's probably fine, but since it feeds the fixed point construction it should be checked. The reliance on [BCLV24] for the Aldous–Lyons implication is external, as stated; the undecidability result here stands on its own.\n\nWho gets value: researchers in quantum complexity, operator algebras, and combinatorics. The paper deserves a serious referee, not a desk rejection. I would recommend sending it to a strong expert on JNV+21-style compression. My own verdict is conditional: I don't see a flaw, but the crux is not yet visible in the first three sections.","headline":"A serious, well-structured claim of TailoredMIP*=RE with the crux deferred to later sections; deserves a rigorous referee.","tokens_in":63891,"tokens_out":2762,"would_cite":true,"duration_ms":28314,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03D35","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"Distinguishing tailored non-local games with perfect strategies from those with quantum value below 1/2 is undecidable.","keywords":["Aldous–Lyons conjecture","tailored non-local games","undecidability","non-sofic unimodular networks","MIP*=RE","compression","probabilistically checkable proofs","Connes embedding problem"],"falsifier":"Take a Turing machine $M$ known independently not to halt, construct $G_M$ from the explicit polynomial-time procedure, and search over finite-dimensional synchronous quantum strategies—for example by an increasing sequence of semidefinite relaxations—for one winning with probability at least 1/2; finding one would falsify the soundness claim. For a halting $M$, checking that the explicit Z-aligned permutation strategy wins all questions is a finite verification whose failure would falsify completeness.","tokens_in":1849,"feed_emoji":"🎲","tokens_out":4151,"duration_ms":162548,"temperature":0.7,"pith_summary":"This paper proves an undecidability gap for tailored non-local games: there is a polynomial-time construction taking any Turing machine $M$ to a tailored non-local game $G_M$ such that $M$ halts exactly when $G_M$ has a perfect Z-aligned permutation strategy that commutes along edges (ZPC). When $M$ never halts, every synchronous quantum strategy wins $G_M$ with probability less than 1/2. This establishes $\\mathrm{TailoredMIP}^* = \\mathrm{RE}$, a strengthening of the earlier $\\mathrm{MIP}^* = \\mathrm{RE}$ theorem, and, via the reduction in the companion paper, implies the existence of non-sofic unimodular networks and therefore refutes the Aldous–Lyons conjecture. It also reproves the negative solution of Connes' embedding problem with a streamlined argument.","feed_headline":"Undecidability of tailored games refutes Aldous–Lyons","feed_subtitle":"Halting machines get tailored games with perfect strategies; non-halting machines leave quantum value below 1/2.","key_machinery":"The load-bearing mechanism is the Compression Theorem, applied to tailored normal-form verifiers (TNFV), finite Turing-machine presentations of tailored games. Compression combines question reduction, answer reduction, and anchored parallel repetition. Question reduction uses an introspection game and a robust self-test of the Pauli group to force the provers to sample their own questions from the right distribution. Answer reduction is a tailor-made probabilistically checkable proof: the players encode their answers in an error-correcting code, and the construction ensures that any encoded bit that depends on an unreadable answer bit does so linearly, because the readable part allows non-linear checks while the unreadable part must remain controlled-linear. The crucial structural fact is that the AND of two Z-aligned permutations is again a Z-aligned permutation, which fails for general permutation strategies. Anchored parallel repetition restores the soundness parameter. The fixed-point verifier $V_{M,\\lambda}$ iterates compression to simulate the Halting problem.","core_discovery":"The central claim is Theorem 2.31: $\\mathrm{TailoredMIP}^* = \\mathrm{RE}$. There is a polynomial-time algorithm that maps a Turing machine $M$ to a tailored non-local game $G_M$ whose question sampling and decision predicate are polynomial-time computable. If $M$ halts, $G_M$ has a perfect Z-aligned permutation strategy that commutes along edges, so $\\mathrm{val}^*(G_M)=1$. If $M$ never halts, $\\mathrm{val}^*(G_M)<1/2$. The theorem is derived from a compression theorem for tailored normal-form verifiers: a reduction in question and answer length that preserves perfect ZPC strategies and amplifies the entanglement needed to win with probability 1/2. The Halting-problem reduction is obtained from a fixed-point verifier that is its own compression exactly until the machine halts.","pith_inferences":["A natural testable follow-up is to run the explicit transformations on a small tailored game such as the magic square game and check whether the perfect ZPC strategy survives compression; this would test the machinery at finite size.","Because the reduction is uniform in $M$, one could in principle search for non-sofic networks at a fixed finite scale by optimizing over the associated tailored games, though no practical algorithm is implied by the proof.","The tailored class may delimit how far proof-checking techniques can be combined with linear constraints: going further toward LCS games would require a new mechanism for encoding non-linear checks, which the paper leaves open."],"forward_implications":["If the theorem is correct, the Aldous–Lyons conjecture is false: the companion reduction converts any tailored game with the Theorem 2.31 gap into a unimodular network that is not sofic.","The same undecidability equality yields non-embeddable II$_1$ factors, giving a negative solution to Connes' embedding problem and to Tsirelson's problem.","The result rules out any effective classification of winnable tailored games: the promise problem that separates perfect ZPC value from low quantum value is RE-complete.","The compression theorem implies that any game below value 1/2 requires exponentially growing entanglement to be won with bounded probability, which is exactly what drives the fixed-point reduction."],"supporting_citations":[{"why":"Companion paper that converts the tailored-game undecidability into non-sofic unimodular networks, refuting the Aldous–Lyons conjecture.","marker":"[BCLV24]"},{"why":"Source of the compression technique and of the earlier MIP*=RE theorem that the present paper strengthens and reproves.","marker":"[JNV+21]"},{"why":"Supplies the stable Pauli-group presentation and simplifications used in the question-reduction step.","marker":"[dlS22b]"},{"why":"Provides the result that converts non-synchronous soundness and entanglement bounds into synchronous ones.","marker":"[Vid22]"},{"why":"Demonstrates obstacles to fully linear answer reduction, motivating the tailored-game middle ground.","marker":"[PS23]"},{"why":"Introduces the introspection technique on which question reduction is based.","marker":"[NW19]"}],"fun_headline_variants":["Halting problem decides perfect tailored-game strategies","Tailored games: perfect strategy is undecidable","Refuting Aldous–Lyons via undecidable tailored games","Halting machines play perfectly in tailored games"],"cache_read_input_tokens":66048,"weakest_assumption_plain":"The main theorem rests on the Compression Theorem; its load-bearing premise is that answer reduction can be implemented for tailored verifiers so that every encoded bit depending on an unreadable answer bit depends on it linearly—if this tailored probabilistic checking step fails, the fixed-point reduction to the Halting problem breaks.","fun_headline_variants_meta":{"raw":{"variants":["Halting problem decides perfect tailored-game strategies","Tailored games: perfect strategy is undecidable","Refuting Aldous–Lyons via undecidable tailored games","Halting machines play perfectly in tailored games"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000185,"raw_usage":{"total_tokens":1380,"prompt_tokens":1059,"completion_tokens":321,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":675,"completion_tokens_details":{"reasoning_tokens":259}},"tokens_in":675,"tokens_out":321,"duration_ms":3949,"temperature":1.0,"reasoning_tokens":259,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T22:57:24.409622+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a Turing machine $M$ known independently not to halt, construct $G_M$ from the explicit polynomial-time procedure, and search over finite-dimensional synchronous quantum strategies—for example by an increasing sequence of semidefinite relaxations—for one winning with probability at least 1/2; finding one would falsify the soundness claim. For a halting $M$, checking that the explicit Z-aligned permutation strategy wins all questions is a finite verification whose failure would falsify completeness.","supporting_citations":[],"review_version":1}